From 485a0a6280abbef62f7e2c2bfbaf3b73d67bbdaf Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 15 Sep 2017 15:23:15 +0200 Subject: Use type Universes.universe_binders. --- interp/declare.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/declare.ml') 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 -- cgit v1.2.3