adapt to coq/coq#19358

LPCIC · Jul 17, 2024 · 0004720 · 0004720
1 parent 48c3020
commit 0004720
Showing 1 changed file with 16 additions and 8 deletions.
diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg
@@ -2025,14 +2025,19 @@ let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) =
 	  let params1, c1, extra_args1 =
 		 match arg with
 		 | Some c -> (* A primitive projection applied to c *)
-			let ty = Retyping.get_type_of ~lax:true env sigma c in
-			let (i,u), ind_args =
-			  (* Are we sure that ty is not an evar? *)
-			  Inductiveops.find_mrectype env sigma ty
-			in ind_args, c, sk1
+      let ty =
+        try Retyping.get_type_of ~lax:true env sigma c with
+        | Retyping.RetypeError _ -> raise Not_found
+      in
+        let ind_args =
+        try
+          Some (Inductiveops.find_mrectype env sigma ty |> snd)
+        with Not_found -> None
+      in
+      ind_args, c, sk1
 		 | None ->
 		 match Reductionops.Stack.strip_n_app structure.nparams sk1 with
-		 | Some (params1, c1, extra_args1) -> (Option.get @@ Reductionops.Stack.list_of_app_stack params1), c1, extra_args1
+		 | Some (params1, c1, extra_args1) -> (Reductionops.Stack.list_of_app_stack params1), c1, extra_args1
        | _ -> raise Not_found in
      let sk2, extra_args2 =
         if Reductionops.Stack.args_size sk2 = Reductionops.Stack.args_size extra_args1 then [], sk2
@@ -2082,9 +2087,13 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
      let sigma, (goal_ty, _) = Evarutil.new_type_evar env sigma Evd.UnivRigid in
 	  let sigma, goal = Evarutil.new_evar env sigma goal_ty in
 	  let goal_evar, _ = EConstr.destEvar sigma goal in
+    let nparams = Structures.Structure.projection_nparams proji in
 	  let query ~depth state =
 		 let state, (loc, q), gls =
-			Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [EConstr.mkApp (EConstr.mkConstU (proji, u), Array.of_list params1); rhs])
+      let lhs = match params1 with
+        | Some params1 -> EConstr.mkApp (EConstr.mkConstU (proji, u), Array.of_list params1)
+        | None -> EConstr.mkConstU (proji, u) in
+			Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [lhs; rhs])
 			  ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
 		 let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in
 		 let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
@@ -2102,7 +2111,6 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) =
 			  let args_type = List.rev_map Context.Rel.Declaration.get_type args_goal in
 			  let args_type = List.map EConstr.of_constr args_type in
            let args = snd (Constr.decompose_app_list t) in
-           let nparams = List.length params1 in
            let params, projs = CList.chop nparams args in
            let i = Structures.Structure.projection_number env proji in
            let lhs = List.nth projs i in