package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val set_minimization : bool ref
val is_set_minimization : unit -> bool
val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds
type universe_binders = (Names.Id.t * Univ.universe_level) list
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
val universe_binders_of_global : Globnames.global_reference -> universe_binders
val set_remote_new_univ_level : Univ.universe_level RemoteCounter.installer
val new_univ_level : Names.dir_path -> Univ.universe_level
val new_univ : Names.dir_path -> Univ.universe
val new_Type : Names.dir_path -> Term.types
val new_Type_sort : Names.dir_path -> Term.sorts
val new_global_univ : unit -> Univ.universe Univ.in_universe_context_set
val new_sort_in_family : Term.sorts_family -> Term.sorts
type universe_constraint_type =
  1. | ULe
  2. | UEq
  3. | ULub
module Constraints : sig ... end
type universe_constraints = Constraints.t
type !'a constraint_accumulator = universe_constraints -> 'a -> 'a option
type !'a universe_constrained = 'a * universe_constraints
type !'a universe_constraint_function = 'a -> 'a -> universe_constraints -> universe_constraints
val subst_univs_universe_constraints : Univ.universe_subst_fn -> universe_constraints -> universe_constraints
val enforce_eq_instances_univs : bool -> Univ.universe_instance universe_constraint_function
val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> Term.constr -> Term.constr -> 'a -> 'a option
val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> Term.constr -> Term.constr -> 'a -> 'a option
val eq_constr_universes : Term.constr -> Term.constr -> universe_constraints option
val leq_constr_universes : Term.constr -> Term.constr -> universe_constraints option
val eq_constr_universes_proj : Environ.env -> Term.constr -> Term.constr -> bool universe_constrained
module UF : sig ... end
type universe_opt_subst = Univ.universe option Univ.universe_map
val subst_opt_univs_constr : universe_opt_subst -> Term.constr -> Term.constr
val normalize_univ_variable_opt_subst : universe_opt_subst ref -> Univ.universe_level -> Univ.universe
val normalize_univ_variable_subst : Univ.universe_subst ref -> Univ.universe_level -> Univ.universe
val normalize_universe_opt_subst : universe_opt_subst ref -> Univ.universe -> Univ.universe
val normalize_universe_subst : Univ.universe_subst ref -> Univ.universe -> Univ.universe
val constr_of_global : Globnames.global_reference -> Term.constr
val constr_of_reference : Globnames.global_reference -> Term.constr
val unsafe_type_of_global : Globnames.global_reference -> Term.types
val nf_evars_and_universes_opt_subst : (Term.existential -> Term.constr option) -> universe_opt_subst -> Term.constr -> Term.constr
val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds
val solve_constraints_system : Univ.universe option array -> Univ.universe array -> Univ.universe array -> Univ.universe array
val univ_inf_ind_from_universe_context : Univ.universe_context -> Univ.cumulativity_info
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