coq 8.8.1 · OCaml Package

module UPairSet : sig ... end

val set_minimization : bool 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 =

| ULe of Univ.Universe.t * Univ.Universe.t
| UEq of Univ.Universe.t * Univ.Universe.t
| ULub of Univ.Level.t * Univ.Level.t
| 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 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

val fresh_instance_from_context : 
  Univ.AUContext.t ->
  Univ.Instance.t Univ.constrained

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

val fresh_sort_in_family : 
  Environ.env ->
  Sorts.family ->
  Sorts.t Univ.in_universe_context_set

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

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

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

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

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

val fresh_universe_context_set_instance : 
  Univ.ContextSet.t ->
  Univ.universe_level_subst * Univ.ContextSet.t

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

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

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

module UF : sig ... end

val level_subst_of : Univ.universe_subst_fn -> Univ.universe_level_subst_fn

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 make_opt_subst : universe_opt_subst -> Univ.universe_subst_fn

val subst_opt_univs_constr : 
  universe_opt_subst ->
  Constr.constr ->
  Constr.constr

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

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

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 ref ->
  Univ.Level.t ->
  Univ.Universe.t

val normalize_univ_variable_subst : 
  Univ.universe_subst ref ->
  Univ.Level.t ->
  Univ.Universe.t

val normalize_universe_opt_subst : 
  universe_opt_subst ref ->
  Univ.Universe.t ->
  Univ.Universe.t

val normalize_universe_subst : 
  Univ.universe_subst 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 type_of_global : 
  Globnames.global_reference ->
  Constr.types Univ.in_universe_context_set

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

package coq