aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/indschemes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/indschemes.ml')
-rw-r--r--vernac/indschemes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index facebd096..90168843a 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -108,7 +108,7 @@ let _ =
let define id internal ctx c t =
let f = declare_constant ~internal in
- let _, univs = Evd.universe_context ctx in
+ let _, univs = Evd.universe_context ~names:[] ~extensible:true ctx in
let univs =
if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
else Monomorphic_const_entry univs