aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/univ.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 117bc4e5fd..2cc57c38ca 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -754,7 +754,7 @@ let is_set_arc u = Level.is_set u.univ
let is_prop_arc u = Level.is_prop u.univ
exception AlreadyDeclared
-
+
let add_universe vlev strict g =
try
let _arcv = UMap.find vlev g in