Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

adapt to coq/coq#19358 #668

Merged
merged 1 commit into from
Oct 1, 2024
Merged

adapt to coq/coq#19358 #668

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 5 additions & 2 deletions apps/cs/src/coq_elpi_cs_hook.mlg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,9 +14,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
Expand All @@ -34,7 +38,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
Expand Down
Loading