Skip to content

Commit

Permalink
Adapt to coq/coq#18852 (interp_red_expr can be done without ltac)
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Mar 28, 2024
1 parent 3eca445 commit 70e4a90
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion template-coq/src/g_template_coq.mlg
Original file line number Diff line number Diff line change
Expand Up @@ -87,7 +87,7 @@ VERNAC COMMAND EXTEND TemplateCoq_Quote_Definition_Eval CLASSIFIED AS SIDEFF STA
{ fun ~pm -> let (env, evm) = fresh_env () in
let (evm, def) = Constrintern.interp_open_constr env evm def in
(* TODO : implem quoting of tactic reductions so that we can use ptmQuoteDefinitionRed *)
let (evm, rd) = Tacinterp.interp_redexp env evm rd in
let (evm, rd) = Redexpr.interp_redexp_no_ltac env evm rd in
let (evm, def) = Plugin_core.reduce env evm rd (to_constr_evars evm def) in
let (evm, pgm) = EConstr.fresh_global env evm (Lazy.force Template_monad.ptmQuoteDefinition) in
let pgm = Constr.mkApp (EConstr.to_constr evm pgm, [|Constr_quoter.quote_ident name; Constr.mkRel 0; def|]) in
Expand Down

0 comments on commit 70e4a90

Please sign in to comment.