Merge pull request #1098 from ppedrot/typecheck-unquote

Typecheck the result of term unquotation.
MetaCoq · Aug 30, 2024 · 3067209 · 3067209
2 parents a08708b + 7bfa901
commit 3067209
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/template-coq/src/g_template_coq.mlg b/template-coq/src/g_template_coq.mlg
@@ -165,6 +165,7 @@ TACTIC EXTEND TemplateCoq_denote_term
          let env = Proofview.Goal.env gl in
          let evm = Proofview.Goal.sigma gl in
          let evm, c = Constr_denoter.denote_term env evm (to_constr_evars evm c) in
+         let evm, _ = Typing.type_of env evm (EConstr.of_constr c) in
          Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evm)
 	   (ltac_apply tac (List.map to_ltac_val [EConstr.of_constr c]))
       end) }