`tmMkDefinition` and friends discard the evar map

[MathisBD]

Calling tmMkDefinition discards the current evar map. Here is the relevant code (in `template-coq/run_template_monad.ml") :

`TmDefininition` case

let name = unquote_ident (reduce_all env evm name) in
let opaque = unquote_bool (reduce_all env evm opaque) in
let evm, typ = (match unquote_option s with Some s -> let red = unquote_reduction_strategy env evm s in Plugin_core.reduce env evm red typ | None -> evm, typ) in
let cinfo = Declare.CInfo.make ~name () ~typ:(Some (EConstr.of_constr typ)) in
let info = Declare.Info.make ~poly ~kind:(Decls.IsDefinition Decls.Definition) () in
let n = Declare.declare_definition ~cinfo ~info ~opaque ~body:(EConstr.of_constr body) evm in
let env = Global.env () in
(* Careful, universes in evm were modified for the declaration of def *)
let evm = Evd.from_env env in
let evm, c = Evd.fresh_global (Global.env ()) evm n in
k ~st env evm (EConstr.to_constr evm c)

And here is a MWE to reproduce the bug :

From MetaCoq.Template Require Import All.
From MetaCoq.Utils Require Import monad_utils.
Import MCMonadNotation.

Unset MetaCoq Strict Unquote Universe Mode.

Definition test :=
  mlet t1 <- tmUnquoteTyped Type (tSort (sType (Universe.make' fresh_level))) ;;
  mlet t2 <- tmUnquoteTyped Type (tSort (sType (Universe.make' fresh_level))) ;;
  tmPrint (t1, t2) ;;
  tmDefinitionRed "t1"%bs None t1 ;;
  tmDefinitionRed "t2"%bs None t2.

Fail MetaCoq Run test.
(* The command has indeed failed with message:
   Undeclared universe: Bug.174 (maybe a bugged tactic).*)

The test function creates two universes (which you can check from the tmPrint output), and the second call to tmDefinitionRed fails because the universe of t2 is undeclared (indeed we discarded the evar map).