diff --git a/template-coq/src/g_template_coq.mlg b/template-coq/src/g_template_coq.mlg index f7e5d7ba4..1a8a1fbd9 100644 --- a/template-coq/src/g_template_coq.mlg +++ b/template-coq/src/g_template_coq.mlg @@ -138,8 +138,9 @@ END VERNAC COMMAND EXTEND TemplateCoq_Run_Template_Program CLASSIFIED AS SIDEFF STATE program | #[ poly = polymorphic ] [ "MetaCoq" "Run" constr(def) ] -> { fun ~pm -> let (env, evm) = fresh_env () in - let (evm, def) = Constrintern.interp_open_constr env evm def in - let pgm = to_constr_evars evm def in + let (pgm, ctx) = Constrintern.interp_constr env evm def in + let evm = Evd.from_ctx ctx in + let pgm = EConstr.to_constr ~abort_on_undefined_evars:true evm pgm in run_template_program ~pm env evm ~poly pgm } END diff --git a/test-suite/issue1042.v b/test-suite/issue1042.v new file mode 100644 index 000000000..819c11f0b --- /dev/null +++ b/test-suite/issue1042.v @@ -0,0 +1,28 @@ +From MetaCoq.Utils Require Import utils. +From MetaCoq.Template Require Import All. +Import MCMonadNotation. + + +(*Exemple with a typing error*) +Definition ident_term (a : term) : term := a. + +Definition quote_inductive {X}(inductive:X): TemplateMonad _ := + quote <- tmQuote inductive;; + tmReturn quote. + +Inductive tm : Set := . + +Definition d1 : TemplateMonad unit. +(* Set Debug "backtrace". *) +Fail MetaCoq Run( + quote <- quote_inductive tm;; + constructor <- ident_term quote;; + tmPrint constructor) +. +Fail run_template_program (quote <- quote_inductive tm;; +constructor <- ident_term quote;; +tmPrint constructor) ltac:(fun x => idtac). + Fail refine ( + quote <- quote_inductive tm;; + constructor <- ident_term quote;; + tmPrint constructor). \ No newline at end of file