diff --git a/template-coq/src/g_template_coq.mlg b/template-coq/src/g_template_coq.mlg index d6d47c30a..97da320db 100644 --- 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) }