aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/declare.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/declare.ml')
-rw-r--r--interp/declare.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 1aeb67afb..0adad1419 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -560,7 +560,7 @@ let do_universe poly l =
ignore(Lib.add_leaf id (input_universe (src, lev))))
l
-type constraint_decl = polymorphic * Univ.constraints
+type constraint_decl = polymorphic * Univ.Constraint.t
let cache_constraints (na, (p, c)) =
let ctx =