coq 8.8.1 · OCaml Package

exception UniversesDiffer

type t

val empty : t

val make : UGraph.t -> t

val make_with_initial_binders : UGraph.t -> Misctypes.lident list -> t

val is_empty : t -> bool

val union : t -> t -> t

val of_context_set : Univ.ContextSet.t -> t

val of_binders : Universes.universe_binders -> t

val universe_binders : t -> Universes.universe_binders

val context_set : t -> Univ.ContextSet.t

val subst : t -> Universes.universe_opt_subst

val ugraph : t -> UGraph.t

val initial_graph : t -> UGraph.t

val algebraics : t -> Univ.LSet.t

val constraints : t -> Univ.Constraint.t

val context : t -> Univ.UContext.t

val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry

val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes

val drop_weak_constraints : bool ref

val add_constraints : t -> Univ.Constraint.t -> t

val add_universe_constraints : t -> Universes.Constraints.t -> t

val universe_of_name : t -> Names.Id.t -> Univ.Level.t

val restrict : t -> Univ.LSet.t -> t

val demote_seff_univs : 
  Safe_typing.private_constants Entries.definition_entry ->
  t ->
  t

type rigid =

| UnivRigid
| UnivFlexible of bool

val univ_rigid : rigid

val univ_flexible : rigid

val univ_flexible_alg : rigid

val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t

val merge_subst : t -> Universes.universe_opt_subst -> t

val emit_side_effects : Safe_typing.private_constants -> t -> t

val new_univ_variable : 
  ?loc:Loc.t ->
  rigid ->
  Names.Id.t option ->
  t ->
  t * Univ.Level.t

val add_global_univ : t -> Univ.Level.t -> t

val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t

val make_flexible_nonalgebraic : t -> t

val is_sort_variable : t -> Sorts.t -> Univ.Level.t option

val normalize_variables : t -> Univ.universe_subst * t

val constrain_variables : Univ.LSet.t -> t -> t

val abstract_undefined_variables : t -> t

val fix_undefined_variables : t -> t

val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst

val minimize : t -> t

val normalize : t -> t

deprecated Alias of UState.minimize

type universe_decl =
  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl

val check_univ_decl : 
  poly:bool ->
  t ->
  universe_decl ->
  Entries.constant_universes_entry

val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t

val update_sigma_env : t -> Environ.env -> t

val pr_uctx_level : t -> Univ.Level.t -> Pp.t

val reference_of_level : t -> Univ.Level.t -> Libnames.reference

val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t

package coq