Merge branch 'coq-8.17' into coq-8.18

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
 

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).