coq 8.7.2 · OCaml Package

exception UniversesDiffer

type t

val empty : t

val make : UGraph.t -> t

val is_empty : t -> bool

val union : t -> t -> t

val of_context_set : Univ.universe_context_set -> t

val of_binders : Universes.universe_binders -> t

val context_set : t -> Univ.universe_context_set

val subst : t -> Universes.universe_opt_subst

val ugraph : t -> UGraph.t

val algebraics : t -> Univ.LSet.t

val constraints : t -> Univ.constraints

val context : t -> Univ.universe_context

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

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

val add_universe_name : t -> string -> Univ.Level.t -> t

val universe_of_name : t -> string -> Univ.Level.t

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

type rigid =

val univ_rigid : rigid

val univ_flexible : rigid

val univ_flexible_alg : rigid

val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.universe_context_set -> 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 ->
  string 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 -> Univ.constraints

val abstract_undefined_variables : t -> t

val fix_undefined_variables : t -> t

val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst

val normalize : t -> t

val universe_context : 
  ?names:Names.Id.t Loc.located list ->
  t ->
  (Names.Id.t * Univ.Level.t) list * Univ.universe_context

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

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

package coq