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 make_with_initial_binders : 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 const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
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 : 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 -> extend: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 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.constant_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
val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t