package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val set_cumulative_sprop : bool -> t -> t
val set_type_in_type : bool -> t -> t
val type_in_type : t -> bool
type !'a check_function = t -> 'a -> 'a -> bool
val check_eq_level : Univ.Level.t check_function
val initial_universes : t
val initial_universes_with : t -> t
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
module Bound : sig ... end
val add_universe : Univ.Level.t -> lbound:Bound.t -> strict: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 choose : (Univ.Level.t -> bool) -> t -> Univ.Level.t -> Univ.Level.t option
val constraints_for : kept:Univ.LSet.t -> t -> Univ.Constraint.t
val domain : t -> Univ.LSet.t
val check_subtype : lbound:Bound.t -> Univ.AUContext.t check_function
val dump_universes : (Univ.constraint_type -> Univ.Level.t -> Univ.Level.t -> unit) -> t -> unit
val check_universes_invariants : t -> unit
OCaml

Innovation. Community. Security.