package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val pr_with_global_universes : Univ.Level.t -> Pp.t
  • deprecated Use [UnivNames.pr_with_global_universes]
val reference_of_level : Univ.Level.t -> Libnames.qualid
  • deprecated Use [UnivNames.qualid_of_level]
val add_global_universe : Univ.Level.t -> Decl_kinds.polymorphic -> unit
  • deprecated Use [UnivNames.add_global_universe]
val is_polymorphic : Univ.Level.t -> bool
  • deprecated Use [UnivNames.is_polymorphic]
type universe_binders = UnivNames.universe_binders
  • deprecated Use [UnivNames.universe_binders]
val empty_binders : universe_binders
  • deprecated Use [UnivNames.empty_binders]
val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
  • deprecated Use [UnivNames.register_universe_binders]
val universe_binders_of_global : Globnames.global_reference -> universe_binders
  • deprecated Use [UnivNames.universe_binders_of_global]
type univ_name_list = UnivNames.univ_name_list
  • deprecated Use [UnivNames.univ_name_list]
val universe_binders_with_opt_names : Globnames.global_reference -> Univ.Level.t list -> univ_name_list option -> universe_binders
  • deprecated Use [UnivNames.universe_binders_with_opt_names]
type universe_id = UnivGen.universe_id
  • deprecated Use [UnivGen.universe_id]
val set_remote_new_univ_id : universe_id RemoteCounter.installer
  • deprecated Use [UnivGen.set_remote_new_univ_id]
val new_univ_id : unit -> universe_id
  • deprecated Use [UnivGen.new_univ_id]
val new_univ_level : unit -> Univ.Level.t
  • deprecated Use [UnivGen.new_univ_level]
val new_univ : unit -> Univ.Universe.t
  • deprecated Use [UnivGen.new_univ]
val new_Type : unit -> Constr.types
  • deprecated Use [UnivGen.new_Type]
val new_Type_sort : unit -> Sorts.t
  • deprecated Use [UnivGen.new_Type_sort]
val new_global_univ : unit -> Univ.Universe.t Univ.in_universe_context_set
  • deprecated Use [UnivGen.new_global_univ]
val new_sort_in_family : Sorts.family -> Sorts.t
  • deprecated Use [UnivGen.new_sort_in_family]
val fresh_instance_from_context : Univ.AUContext.t -> Univ.Instance.t Univ.constrained
  • deprecated Use [UnivGen.fresh_instance_from_context]
  • deprecated Use [UnivGen.fresh_instance_from]
val fresh_sort_in_family : Sorts.family -> Sorts.t Univ.in_universe_context_set
  • deprecated Use [UnivGen.fresh_sort_in_family]
  • deprecated Use [UnivGen.fresh_constant_instance]
  • deprecated Use [UnivGen.fresh_inductive_instance]
  • deprecated Use [UnivGen.fresh_constructor_instance]
  • deprecated Use [UnivGen.fresh_global_instance]
  • deprecated Use [UnivGen.fresh_global_or_constr_instance]
val fresh_universe_context_set_instance : Univ.ContextSet.t -> Univ.universe_level_subst * Univ.ContextSet.t
  • deprecated Use [UnivGen.fresh_universe_context_set_instance]
  • deprecated Use [UnivGen.global_of_constr]
  • deprecated Use [UnivGen.constr_of_global_univ]
  • deprecated Use [UnivGen.extend_context]
val constr_of_global : Globnames.global_reference -> Constr.constr
  • deprecated Use [UnivGen.constr_of_global]
val constr_of_reference : Globnames.global_reference -> Constr.constr
  • deprecated Use [UnivGen.constr_of_global]
  • deprecated Use [UnivGen.type_of_global]
  • deprecated Use [UnivSubst.level_subst_of]
val subst_univs_constraints : Univ.universe_subst_fn -> Univ.Constraint.t -> Univ.Constraint.t
  • deprecated Use [UnivSubst.subst_univs_constraints]
val subst_univs_constr : Univ.universe_subst -> Constr.constr -> Constr.constr
  • deprecated Use [UnivSubst.subst_univs_constr]
type universe_opt_subst = UnivSubst.universe_opt_subst
  • deprecated Use [UnivSubst.universe_opt_subst]
  • deprecated Use [UnivSubst.make_opt_subst]
val subst_opt_univs_constr : universe_opt_subst -> Constr.constr -> Constr.constr
  • deprecated Use [UnivSubst.subst_opt_univs_constr]
  • deprecated Use [UnivSubst.normalize_univ_variables]
val normalize_univ_variable : find:(Univ.Level.t -> Univ.Universe.t) -> Univ.Level.t -> Univ.Universe.t
  • deprecated Use [UnivSubst.normalize_univ_variable]
val normalize_univ_variable_opt_subst : universe_opt_subst -> Univ.Level.t -> Univ.Universe.t
  • deprecated Use [UnivSubst.normalize_univ_variable_opt_subst]
val normalize_univ_variable_subst : Univ.universe_subst -> Univ.Level.t -> Univ.Universe.t
  • deprecated Use [UnivSubst.normalize_univ_variable_subst]
val normalize_universe_opt_subst : universe_opt_subst -> Univ.Universe.t -> Univ.Universe.t
  • deprecated Use [UnivSubst.normalize_universe_opt_subst]
val normalize_universe_subst : Univ.universe_subst -> Univ.Universe.t -> Univ.Universe.t
  • deprecated Use [UnivSubst.normalize_universe_subst]
val nf_evars_and_universes_opt_subst : (Constr.existential -> Constr.constr option) -> universe_opt_subst -> Constr.constr -> Constr.constr
  • deprecated Use [UnivSubst.nf_evars_and_universes_opt_subst]
val pr_universe_opt_subst : universe_opt_subst -> Pp.t
  • deprecated Use [UnivSubst.pr_universe_opt_subst]
type universe_constraint = UnivProblem.t =
  1. | ULe of Univ.Universe.t * Univ.Universe.t
    (*
    • deprecated Use [UnivProblem.ULe]
    *)
  2. | UEq of Univ.Universe.t * Univ.Universe.t
    (*
    • deprecated Use [UnivProblem.UEq]
    *)
  3. | ULub of Univ.Level.t * Univ.Level.t
    (*
    • deprecated Use [UnivProblem.ULub]
    *)
  4. | UWeak of Univ.Level.t * Univ.Level.t
    (*
    • deprecated Use [UnivProblem.UWeak]
    *)
  • deprecated Use [UnivProblem.t]
module Constraints = UnivProblem.Set
type !'a constraint_accumulator = 'a UnivProblem.accumulator
  • deprecated Use [UnivProblem.accumulator]
type !'a universe_constrained = 'a UnivProblem.constrained
  • deprecated Use [UnivProblem.constrained]
type !'a universe_constraint_function = 'a UnivProblem.constraint_function
  • deprecated Use [UnivProblem.constraint_function]
val subst_univs_universe_constraints : Univ.universe_subst_fn -> Constraints.t -> Constraints.t
  • deprecated Use [UnivProblem.Set.subst_univs]
val enforce_eq_instances_univs : bool -> Univ.Instance.t universe_constraint_function
  • deprecated Use [UnivProblem.enforce_eq_instances_univs]
val to_constraints : force_weak:bool -> UGraph.t -> Constraints.t -> Univ.Constraint.t
  • deprecated Use [UnivProblem.to_constraints]
  • deprecated Use [UnivProblem.eq_constr_univs_infer_with]
module UPairSet = UnivMinim.UPairSet
  • deprecated Use [UnivMinim.normalize_context_set]