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.

Author: ppedrot

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