aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3bac4a6555..476db06c54 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -380,7 +380,7 @@ let context poly l =
begin
let uctx = Evd.universe_context_set sigma in
Declare.declare_universe_context poly uctx;
- if poly then Polymorphic_const_entry ([], Univ.UContext.empty)
+ if poly then Polymorphic_const_entry ([||], Univ.UContext.empty)
else Monomorphic_const_entry Univ.ContextSet.empty
end
else if poly then