package coq

You can search for identifiers within the package.

in-package search v0.2.0

Package contains no libraries

type t

type universes = t

type !'a check_function = universes -> 'a -> 'a -> bool

val check_leq : Univ.universe check_function

val check_eq : Univ.universe check_function

val check_eq_level : Univ.universe_level check_function

val empty_universes : universes

val initial_universes : universes

val is_initial_universes : universes -> bool

val sort_universes : universes -> universes

exception AlreadyDeclared

val add_universe : Univ.universe_level -> bool -> universes -> universes

val enforce_constraint : Univ.univ_constraint -> universes -> universes

val merge_constraints : Univ.constraints -> universes -> universes

val constraints_of_universes : universes -> Univ.constraints

val check_constraint : universes -> Univ.univ_constraint -> bool

val check_constraints : Univ.constraints -> universes -> bool

val check_eq_instances : Univ.Instance.t check_function

val pr_universes : 
  (Univ.Level.t -> Pp.std_ppcmds) ->
  universes ->
  Pp.std_ppcmds

val dump_universes : 
  (Univ.constraint_type -> string -> string -> unit) ->
  universes ->
  unit

val check_universes_invariants : universes -> unit