package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
module UPairSet : sig ... end
val set_minimization : bool Pervasives.ref
val is_set_minimization : unit -> bool
val pr_with_global_universes : Univ.Level.t -> Pp.t
val reference_of_level : Univ.Level.t -> Libnames.reference
val add_global_universe : Univ.Level.t -> Decl_kinds.polymorphic -> unit
val is_polymorphic : Univ.Level.t -> bool
type universe_binders = Univ.Level.t Names.Id.Map.t
val empty_binders : universe_binders
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
val universe_binders_of_global : Globnames.global_reference -> universe_binders
type univ_name_list = Misctypes.lname list
val universe_binders_with_opt_names : Globnames.global_reference -> Univ.Level.t list -> univ_name_list option -> universe_binders
type universe_id = Names.DirPath.t * int
val set_remote_new_univ_id : universe_id RemoteCounter.installer
val new_univ_id : unit -> universe_id
val new_univ_level : unit -> Univ.Level.t
val new_univ : unit -> Univ.Universe.t
val new_Type : unit -> Constr.types
val new_Type_sort : unit -> Sorts.t
val new_global_univ : unit -> Univ.Universe.t Univ.in_universe_context_set
val new_sort_in_family : Sorts.family -> Sorts.t
type universe_constraint =
  1. | ULe of Univ.Universe.t * Univ.Universe.t
  2. | UEq of Univ.Universe.t * Univ.Universe.t
  3. | ULub of Univ.Level.t * Univ.Level.t
  4. | UWeak of Univ.Level.t * Univ.Level.t
module Constraints : sig ... end
type universe_constraints = Constraints.t
  • deprecated Use Constraints.t
type !'a constraint_accumulator = Constraints.t -> 'a -> 'a option
type !'a universe_constrained = 'a * Constraints.t
type !'a universe_constraint_function = 'a -> 'a -> Constraints.t -> Constraints.t
val subst_univs_universe_constraints : Univ.universe_subst_fn -> Constraints.t -> Constraints.t
val enforce_eq_instances_univs : bool -> Univ.Instance.t universe_constraint_function
val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Univ.Constraint.t
val fresh_instance_from_context : Univ.AUContext.t -> Univ.Instance.t Univ.constrained
val fresh_universe_context_set_instance : Univ.ContextSet.t -> Univ.universe_level_subst * Univ.ContextSet.t
module UF : sig ... end
val subst_univs_constraints : Univ.universe_subst_fn -> Univ.Constraint.t -> Univ.Constraint.t
val subst_univs_constr : Univ.universe_subst -> Constr.constr -> Constr.constr
type universe_opt_subst = Univ.Universe.t option Univ.universe_map
val subst_opt_univs_constr : universe_opt_subst -> Constr.constr -> Constr.constr
val normalize_univ_variable : find:(Univ.Level.t -> Univ.Universe.t) -> update:(Univ.Level.t -> Univ.Universe.t -> Univ.Universe.t) -> Univ.Level.t -> Univ.Universe.t
val normalize_univ_variable_opt_subst : universe_opt_subst Pervasives.ref -> Univ.Level.t -> Univ.Universe.t
val normalize_univ_variable_subst : Univ.universe_subst Pervasives.ref -> Univ.Level.t -> Univ.Universe.t
val normalize_universe_opt_subst : universe_opt_subst Pervasives.ref -> Univ.Universe.t -> Univ.Universe.t
val constr_of_global : Globnames.global_reference -> Constr.constr
val constr_of_reference : Globnames.global_reference -> Constr.constr
  • deprecated synonym of [constr_of_global]
val nf_evars_and_universes_opt_subst : (Constr.existential -> Constr.constr option) -> universe_opt_subst -> Constr.constr -> Constr.constr
val refresh_constraints : UGraph.t -> Univ.ContextSet.t -> Univ.ContextSet.t * UGraph.t
val pr_universe_opt_subst : universe_opt_subst -> Pp.t
val solve_constraints_system : Univ.Universe.t option array -> Univ.Universe.t array -> Univ.Universe.t array -> Univ.Universe.t array
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