Imported Upstream version 8.5~beta3+dfsg

1 files changed, 19 insertions, 0 deletions

diff --git a/library/universes.mli b/library/universes.mli
index 252648d7..45672ef4 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -12,8 +12,12 @@ open Term
 open Environ
 open Univ
 
+val set_minimization : bool ref
+val is_set_minimization : unit -> bool
+
 (** Universes *)
 
+(** Global universe name <-> level mapping *)
 type universe_names = 
   Univ.universe_level Idmap.t * Id.t Univ.LMap.t
 
@@ -22,6 +26,13 @@ val set_global_universe_names : universe_names -> unit
 
 val pr_with_global_universes : Level.t -> Pp.std_ppcmds
 
+(** Local universe name <-> level mapping *)
+
+type universe_binders = (Id.t * Univ.universe_level) list
+					   
+val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
+val universe_binders_of_global : Globnames.global_reference -> universe_binders
+
 (** The global universe counter *)
 val set_remote_new_univ_level : universe_level RemoteCounter.installer
 
@@ -66,6 +77,14 @@ val to_constraints : universes -> universe_constraints -> constraints
    application grouping, the universe constraints in [u] and additional constraints [c]. *)
 val eq_constr_univs_infer : Univ.universes -> constr -> constr -> bool universe_constrained
 
+(** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of
+    {!eq_constr_univs_infer} taking kind-of-term functions, to expose
+    subterms of [m] and [n], arguments. *)
+val eq_constr_univs_infer_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  Univ.universes -> constr -> constr -> bool universe_constrained
+
 (** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b]
     modulo alpha, casts, application grouping, the universe constraints
     in [u] and additional constraints [c]. *)