package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
type universes = t
  • deprecated Use UGraph.t
type !'a check_function = t -> 'a -> 'a -> bool
val check_eq_level : Univ.Level.t check_function
val initial_universes : t
val is_initial_universes : t -> bool
val check_eq_instances : Univ.Instance.t check_function
val enforce_constraint : Univ.univ_constraint -> t -> t
val merge_constraints : Univ.Constraint.t -> t -> t
val check_constraint : t -> Univ.univ_constraint -> bool
val check_constraints : Univ.Constraint.t -> t -> bool
val enforce_leq_alg : Univ.Universe.t -> Univ.Universe.t -> t -> Univ.Constraint.t * t
exception AlreadyDeclared
val add_universe : Univ.Level.t -> bool -> t -> t
val add_universe_unconstrained : Univ.Level.t -> t -> t
exception UndeclaredLevel of Univ.Level.t
val check_declared_universes : t -> Univ.LSet.t -> unit
val pr_universes : (Univ.Level.t -> Pp.t) -> t -> Pp.t
val empty_universes : t
val sort_universes : t -> t
val constraints_of_universes : t -> Univ.Constraint.t * Univ.LSet.t list
val constraints_for : kept:Univ.LSet.t -> t -> Univ.Constraint.t
val check_subtype : Univ.AUContext.t check_function
val dump_universes : (Univ.constraint_type -> string -> string -> unit) -> t -> unit
val check_universes_invariants : t -> unit