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 : lbound:Univ.Level.t -> UGraph.t -> t
val make_with_initial_binders : lbound:Univ.Level.t -> UGraph.t -> Names.lident list -> t
val is_empty : t -> bool
val union : t -> t -> t
val of_context_set : Univ.ContextSet.t -> t
val of_binders : UnivNames.universe_binders -> t
val universe_binders : t -> UnivNames.universe_binders
val context_set : t -> Univ.ContextSet.t
val ugraph : t -> UGraph.t
val initial_graph : t -> UGraph.t
val algebraics : t -> Univ.LSet.t
val constraints : t -> Univ.Constraint.t
val context : t -> Univ.UContext.t
val univ_entry : poly:bool -> t -> Entries.universes_entry
val drop_weak_constraints : bool ref
val add_constraints : t -> Univ.Constraint.t -> t
val add_universe_constraints : t -> UnivProblem.Set.t -> t
val universe_of_name : t -> Names.Id.t -> Univ.Level.t
val restrict_universe_context : lbound:Univ.Level.t -> Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t
val restrict : t -> Univ.LSet.t -> 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 -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> UnivSubst.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
val demote_seff_univs : Univ.LSet.t -> t -> t
val new_univ_variable : ?loc:Loc.t -> rigid -> Names.Id.t 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_nonalgebraic_variable : t -> 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 -> t
val abstract_undefined_variables : t -> t
val fix_undefined_variables : t -> t
val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
val minimize : t -> t
type (!'a, !'b) gen_universe_decl = {
  1. univdecl_instance : 'a;
  2. univdecl_extensible_instance : bool;
  3. univdecl_constraints : 'b;
  4. univdecl_extensible_constraints : bool;
}
type universe_decl = (Names.lident list, Univ.Constraint.t) gen_universe_decl
val default_univ_decl : universe_decl
val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry
val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
val update_sigma_env : t -> Environ.env -> t
val pr_uctx_level : t -> Univ.Level.t -> Pp.t
val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid option
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t
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