diff options
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 34 |
1 files changed, 23 insertions, 11 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 1401c4ee8..1a98d969b 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -18,6 +18,13 @@ val is_set_minimization : unit -> bool (** Universes *) val pr_with_global_universes : Level.t -> Pp.t +val reference_of_level : Level.t -> Libnames.reference + +(** Global universe information outside the kernel, to handle + polymorphic universes in sections that have to be discharged. *) +val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit + +val is_polymorphic : Level.t -> bool (** Local universe name <-> level mapping *) @@ -40,14 +47,17 @@ val universe_binders_with_opt_names : Globnames.global_reference -> Univ.Level.t list -> univ_name_list option -> universe_binders (** The global universe counter *) -val set_remote_new_univ_level : Level.t RemoteCounter.installer +type universe_id = DirPath.t * int + +val set_remote_new_univ_id : universe_id RemoteCounter.installer (** Side-effecting functions creating new universe levels. *) -val new_univ_level : DirPath.t -> Level.t -val new_univ : DirPath.t -> Universe.t -val new_Type : DirPath.t -> types -val new_Type_sort : DirPath.t -> Sorts.t +val new_univ_id : unit -> universe_id +val new_univ_level : unit -> Level.t +val new_univ : unit -> Universe.t +val new_Type : unit -> types +val new_Type_sort : unit -> Sorts.t val new_global_univ : unit -> Universe.t in_universe_context_set val new_sort_in_family : Sorts.family -> Sorts.t @@ -64,21 +74,23 @@ type universe_constraint_type = ULe | UEq | ULub type universe_constraint = Universe.t * universe_constraint_type * Universe.t module Constraints : sig include Set.S with type elt = universe_constraint - + val pr : t -> Pp.t end type universe_constraints = Constraints.t -type 'a constraint_accumulator = universe_constraints -> 'a -> 'a option -type 'a universe_constrained = 'a * universe_constraints -type 'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints +[@@ocaml.deprecated "Use Constraints.t"] + +type 'a constraint_accumulator = Constraints.t -> 'a -> 'a option +type 'a universe_constrained = 'a * Constraints.t +type 'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t val subst_univs_universe_constraints : universe_subst_fn -> - universe_constraints -> universe_constraints + Constraints.t -> Constraints.t val enforce_eq_instances_univs : bool -> Instance.t universe_constraint_function -val to_constraints : UGraph.t -> universe_constraints -> constraints +val to_constraints : UGraph.t -> Constraints.t -> Constraint.t (** [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 |