We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 52fda99 commit a1a1a1bCopy full SHA for a1a1a1b
template-coq/src/constr_denoter.ml
@@ -168,7 +168,7 @@ struct
168
(* TODO handle univs created in workers *)
169
let l = Univ.Level.make (Univ.UGlobal.make dp "" num) in
170
try
171
- let evm = Evd.add_global_univ evm l in
+ let evm = Evd.add_forgotten_univ evm l in
172
if !strict_unquote_universe_mode then
173
CErrors.user_err (str ("Level "^s^" is not a declared level and you are in Strict Unquote Universe Mode."))
174
else (evm, l)
0 commit comments