diff options
Diffstat (limited to 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 19 |
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]. *) |