aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-15 15:23:15 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-24 19:18:56 +0100
commit485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf (patch)
tree5cd5182505dbb5ff9e86610bc74e5ce9f99bfd65 /interp
parentc1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff)
Use type Universes.universe_binders.
Diffstat (limited to 'interp')
-rw-r--r--interp/declare.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 1a589897b..7ab13b859 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -457,7 +457,7 @@ let declare_universe_context poly ctx =
Lib.add_anonymous_leaf (input_universe_context (poly, ctx))
(* Discharged or not *)
-type universe_decl = polymorphic * (Id.t * Univ.Level.t) list
+type universe_decl = polymorphic * Universes.universe_binders
let cache_universes (p, l) =
let glob = Global.global_universe_names () in