coq 8.9.1 · OCaml Package

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]

val fresh_instance_from : 
  Univ.AUContext.t ->
  Univ.Instance.t option ->
  Univ.Instance.t Univ.in_universe_context_set

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]

val fresh_constant_instance : 
  Environ.env ->
  Names.Constant.t ->
  Constr.pconstant Univ.in_universe_context_set

deprecated Use [UnivGen.fresh_constant_instance]

val fresh_inductive_instance : 
  Environ.env ->
  Names.inductive ->
  Constr.pinductive Univ.in_universe_context_set

deprecated Use [UnivGen.fresh_inductive_instance]

val fresh_constructor_instance : 
  Environ.env ->
  Names.constructor ->
  Constr.pconstructor Univ.in_universe_context_set

deprecated Use [UnivGen.fresh_constructor_instance]

val fresh_global_instance : 
  ?names:Univ.Instance.t ->
  Environ.env ->
  Globnames.global_reference ->
  Constr.constr Univ.in_universe_context_set

deprecated Use [UnivGen.fresh_global_instance]

val fresh_global_or_constr_instance : 
  Environ.env ->
  Globnames.global_reference_or_constr ->
  Constr.constr Univ.in_universe_context_set

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]

val global_of_constr : 
  Constr.constr ->
  Globnames.global_reference Univ.puniverses

deprecated Use [UnivGen.global_of_constr]

val constr_of_global_univ : 
  Globnames.global_reference Univ.puniverses ->
  Constr.constr

deprecated Use [UnivGen.constr_of_global_univ]

val extend_context : 
  'a Univ.in_universe_context_set ->
  Univ.ContextSet.t ->
  'a Univ.in_universe_context_set

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]

val type_of_global : 
  Globnames.global_reference ->
  Constr.types Univ.in_universe_context_set

deprecated Use [UnivGen.type_of_global]

val level_subst_of : Univ.universe_subst_fn -> Univ.universe_level_subst_fn

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]

val make_opt_subst : universe_opt_subst -> Univ.universe_subst_fn

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]

val normalize_univ_variables : 
  universe_opt_subst ->
  universe_opt_subst * Univ.LSet.t * Univ.universe_subst

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 =

| ULe of Univ.Universe.t * Univ.Universe.t
(*
- deprecated Use [UnivProblem.ULe]
*)
| UEq of Univ.Universe.t * Univ.Universe.t
(*
- deprecated Use [UnivProblem.UEq]
*)
| ULub of Univ.Level.t * Univ.Level.t
(*
- deprecated Use [UnivProblem.ULub]
*)
| 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]

val eq_constr_univs_infer_with : 
  (Constr.constr ->
    (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) Constr.kind_of_term) ->
  (Constr.constr ->
    (Constr.constr, Constr.types, Sorts.t, Univ.Instance.t) Constr.kind_of_term) ->
  UGraph.t ->
  'a constraint_accumulator ->
  Constr.constr ->
  Constr.constr ->
  'a ->
  'a option

deprecated Use [UnivProblem.eq_constr_univs_infer_with]

module UPairSet = UnivMinim.UPairSet

val normalize_context_set : 
  UGraph.t ->
  Univ.ContextSet.t ->
  universe_opt_subst ->
  Univ.LSet.t ->
  UPairSet.t ->
  (universe_opt_subst * Univ.LSet.t) Univ.in_universe_context_set

deprecated Use [UnivMinim.normalize_context_set]

package coq