diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
index a3076af18..a341ecf5e 100644
--- a/template-coq/src/plugin_core.ml
+++ b/template-coq/src/plugin_core.ml
@@ -90,7 +90,7 @@ let tmDefinition (nm : ident) ?poly:(poly=false) ?opaque:(opaque=false) (typ : t
     let info = Declare.Info.make ~poly ~kind:(Decls.(IsDefinition Definition)) () in
     let n = Declare.declare_definition ~cinfo ~info ~opaque ~body:(EConstr.of_constr body) evm in
     let env = Global.env () in
-    let evm = Evd.from_env env in
+    let evm = Evd.update_sigma_univs (Environ.universes env) evm in
     success ~st env evm (Names.Constant.canonical (Globnames.destConstRef n))
 
 let tmAxiom (nm : ident) ?poly:(poly=false) (typ : term) : kername tm =
@@ -105,7 +105,9 @@ let tmAxiom (nm : ident) ?poly:(poly=false) (typ : term) : kername tm =
         ~kind:(Decls.IsDefinition Decls.Definition)
         param
     in
-    success ~st (Global.env ()) evm (Names.Constant.canonical n)
+    let env = Global.env () in
+    let evm = Evd.update_sigma_univs (Environ.universes env) evm in
+    success ~st env evm (Names.Constant.canonical n)
 
 (* this generates a lemma leaving a hole *)
 let tmLemma (nm : ident) ?poly:(poly=false)(ty : term) : kername tm =
diff --git a/template-coq/src/run_template_monad.ml b/template-coq/src/run_template_monad.ml
index 99e13bc73..35e0f16b5 100644
--- a/template-coq/src/run_template_monad.ml
+++ b/template-coq/src/run_template_monad.ml
@@ -358,6 +358,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
       let empty_mono_univ_entry = UState.Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders in
       Declare.declare_variable ~typing_flags:None ~name ~kind (SectionLocalAssum { typ; impl=Glob_term.Explicit; univs=empty_mono_univ_entry });
       let env = Global.env () in
+      let evm = Evd.update_sigma_univs (Environ.universes env) evm in
       k ~st env evm (Lazy.force unit_tt)
   | TmDefinition (opaque,name,s,typ,body) ->
     if intactic
@@ -369,10 +370,10 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
       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
+      let env = Global.env () in
+      let evm = Evd.update_sigma_univs (Environ.universes env) evm in
+      let evm, c = Evd.fresh_global env evm n in
       k ~st env evm (EConstr.to_constr evm c)
   | TmDefinitionTerm (opaque, name, typ, body) ->
     if intactic
@@ -409,6 +410,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
       let param = Declare.ParameterEntry entry in
       let n = Declare.declare_constant ~name ~kind:Decls.(IsDefinition Definition) param in
       let env = Global.env () in
+      let evm = Evd.update_sigma_univs (Environ.universes env) evm in
       k ~st env evm (Constr.mkConstU (n, UVars.Instance.empty))
   | TmAxiomTerm (name,typ) ->
     if intactic
@@ -534,6 +536,7 @@ let rec run_template_program_rec ~poly ?(intactic=false) (k : Constr.t Plugin_co
     let infer_univs = unquote_bool (reduce_all env evm b) in
     let evm = declare_inductive env evm infer_univs mind in
     let env = Global.env () in
+    let evm = Evd.update_sigma_univs (Environ.universes env) evm in  
     k ~st env evm (Lazy.force unit_tt)
   | TmUnquote t ->
     begin
diff --git a/test-suite/bug_mk_def.v b/test-suite/bug_mk_def.v
new file mode 100644
index 000000000..a8e49e5de
--- /dev/null
+++ b/test-suite/bug_mk_def.v
@@ -0,0 +1,15 @@
+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.
+
+MetaCoq Run test.
+  
\ No newline at end of file