Typecheck the result of term unquotation.

[ppedrot]

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.

cc @tabareau

[ppedrot]

CI green and this works on my branch, so let's merge.

[JasonGross]

Does this fix #842 ? What about #853 ? #862 ?

[JasonGross]

And maybe we can remove

metacoq/quotation/theories/CommonUtils.v

Lines 336 to 341 in b1b6be2

	(* Hack around https://github.com/MetaCoq/metacoq/issues/853 *)
	Definition tmRetypeAroundMetaCoqBug853 (prefix : string) (t : typed_term) : TemplateMonad typed_term
	:= let '{| my_projT1 := ty ; my_projT2 := v |} := t in
	ty <- tmRetypeRelaxOnlyType prefix ty;;
	v <- tmRetypeMagicRelaxOnlyType prefix ty v;;
	ret {| my_projT1 := ty ; my_projT2 := v |}.

[ppedrot]

This only fixes the Ltac binding for denote_term and does not do anything for the vernac commands or the monad evaluator. Typing unconditionally in the constr denoter uncovers bugs in some parts where the environment passed is not the correct one. That is, it produces unbound rels errors. This can be fixed but it requires more work and I wanted the least disruptive change to proceed with coq/coq#19228.