package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val set_minimization : bool Pervasives.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 Pervasives.ref -> Univ.universe_level -> Univ.universe
val normalize_univ_variable_subst : Univ.universe_subst Pervasives.ref -> Univ.universe_level -> Univ.universe
val normalize_universe_opt_subst : universe_opt_subst Pervasives.ref -> Univ.universe -> Univ.universe
val normalize_universe_subst : Univ.universe_subst Pervasives.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.