From f272677ef92b73a9c636926ad30bb604c164de75 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Jul 2024 10:21:22 +0200 Subject: [PATCH] adapt to coq/coq#19358 --- apps/cs/src/coq_elpi_cs_hook.mlg | 29 ++++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index c94e63dcc..0b277f85e 100644 --- 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 @@ -2042,9 +2047,12 @@ let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) = let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list sk2 Reductionops.Stack.empty) in let sigma, goal = Evarutil.new_evar env sigma (Retyping.get_type_of env sigma c1) in let goal_evar, _ = EConstr.destEvar sigma goal in + let lhs = match params1 with + | Some params1 -> EConstr.mkApp (EConstr.mkConstU (proji, u), Array.of_list params1) + | None -> EConstr.mkConstU (proji, u) 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, EConstr.EInstance.empty), Array.of_list params1); rhs]) + 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 @@ -2082,9 +2090,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 +2114,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