Merge pull request #1096 from SkySkimmer/more-demote

Adapt to coq/coq#19384 (add_global_univ -> add_forgotten_univ)
MetaCoq · Jul 24, 2024 · 1d5976a · 1d5976a
2 parents 52fda99 + a1a1a1b
commit 1d5976a
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/template-coq/src/constr_denoter.ml b/template-coq/src/constr_denoter.ml
@@ -168,7 +168,7 @@ struct
         (* TODO handle univs created in workers *)
         let l = Univ.Level.make (Univ.UGlobal.make dp "" num) in
         try
-          let evm = Evd.add_global_univ evm l in
+          let evm = Evd.add_forgotten_univ evm l in
           if !strict_unquote_universe_mode then
             CErrors.user_err (str ("Level "^s^" is not a declared level and you are in Strict Unquote Universe Mode."))
           else (evm, l)