From 7bfa901bffa23ccc07a9f71d03865aeb67281112 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 30 Aug 2024 17:07:07 +0200 Subject: [PATCH] Typecheck the result of term unquotation. In some cases, unquoting could generate terms that were ill-typed, typically when unquoting [I @hole] for some template polymorphic inductive type [I]. Similarly universe levels were not computed at all, which could have led to bizarre failures. To ensure that the unquoted term makes sense at all, we simply perform a call to Typing before returning it. This has a non-trivial cost but since building the term is already linear, this should not hopefully matter that much in practice. --- template-coq/src/g_template_coq.mlg | 1 + 1 file changed, 1 insertion(+) 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) }