package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 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 =
  1. | UnivRigid
  2. | 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.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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct