coq 8.7.2 · OCaml Package

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 =

| ULe
| UEq
| ULub

type universe_constraint =
  Univ.universe * universe_constraint_type * Univ.universe

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 to_constraints : UGraph.t -> universe_constraints -> Univ.constraints

val eq_constr_univs_infer : 
  UGraph.t ->
  'a constraint_accumulator ->
  Term.constr ->
  Term.constr ->
  'a ->
  'a option

val eq_constr_univs_infer_with : 
  (Term.constr ->
    (Term.constr, Term.types, Sorts.t, Univ.Instance.t) Term.kind_of_term) ->
  (Term.constr ->
    (Term.constr, Term.types, Sorts.t, Univ.Instance.t) Term.kind_of_term) ->
  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

val fresh_instance_from_context : 
  Univ.abstract_universe_context ->
  Univ.universe_instance Univ.constrained

val fresh_instance_from : 
  Univ.abstract_universe_context ->
  Univ.universe_instance option ->
  Univ.universe_instance Univ.in_universe_context_set

val fresh_sort_in_family : 
  Environ.env ->
  Term.sorts_family ->
  Term.sorts Univ.in_universe_context_set

val fresh_constant_instance : 
  Environ.env ->
  Names.constant ->
  Term.pconstant Univ.in_universe_context_set

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

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

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

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

val fresh_universe_context_set_instance : 
  Univ.universe_context_set ->
  Univ.universe_level_subst * Univ.universe_context_set

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

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

val extend_context : 
  'a Univ.in_universe_context_set ->
  Univ.universe_context_set ->
  'a Univ.in_universe_context_set

module UF : sig ... end

type universe_opt_subst = Univ.universe option Univ.universe_map

val make_opt_subst : universe_opt_subst -> Univ.universe_subst_fn

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

val normalize_context_set : 
  Univ.universe_context_set ->
  universe_opt_subst ->
  Univ.universe_set ->
  (universe_opt_subst * Univ.universe_set) Univ.in_universe_context_set

val normalize_univ_variables : 
  universe_opt_subst ->
  universe_opt_subst
  * Univ.universe_set
  * Univ.universe_set
  * Univ.universe_subst

val normalize_univ_variable : 
  find:(Univ.universe_level -> Univ.universe) ->
  update:(Univ.universe_level -> Univ.universe -> Univ.universe) ->
  Univ.universe_level ->
  Univ.universe

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_constr_of_global : 
  Globnames.global_reference ->
  Term.constr Univ.in_universe_context

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

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 refresh_constraints : 
  UGraph.t ->
  Univ.universe_context_set ->
  Univ.universe_context_set * UGraph.t

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

package coq