coq 8.7.1 · OCaml Package

module Level : sig ... end

type universe_level = Level.t

module LSet : sig ... end

type universe_set = LSet.t

module Universe : sig ... end

type universe = Universe.t

val pr_uni : universe -> Pp.std_ppcmds

val type0m_univ : universe

val type0_univ : universe

val type1_univ : universe

val is_type0_univ : universe -> bool

val is_type0m_univ : universe -> bool

val is_univ_variable : universe -> bool

val is_small_univ : universe -> bool

val sup : universe -> universe -> universe

val super : universe -> universe

val universe_level : universe -> universe_level option

val univ_level_mem : universe_level -> universe -> bool

val univ_level_rem : universe_level -> universe -> universe -> universe

type constraint_type =

| Lt
| Le
| Eq

type univ_constraint = universe_level * constraint_type * universe_level

module Constraint : sig ... end

type constraints = Constraint.t

val empty_constraint : constraints

val union_constraint : constraints -> constraints -> constraints

val eq_constraint : constraints -> constraints -> bool

type !'a constrained = 'a * constraints

val constraints_of : 'a constrained -> constraints

type !'a constraint_function = 'a -> 'a -> constraints -> constraints

val enforce_eq : universe constraint_function

val enforce_leq : universe constraint_function

val enforce_eq_level : universe_level constraint_function

val enforce_leq_level : universe_level constraint_function

type explanation = (constraint_type * universe) list

type univ_inconsistency =
  constraint_type * universe * universe * explanation option

exception UniverseInconsistency of univ_inconsistency

module LMap : sig ... end

type 'a universe_map = 'a LMap.t

type universe_subst_fn = universe_level -> universe

type universe_level_subst_fn = universe_level -> universe_level

type universe_subst = universe universe_map

type universe_level_subst = universe_level universe_map

val level_subst_of : universe_subst_fn -> universe_level_subst_fn

module Instance : sig ... end

type universe_instance = Instance.t

val enforce_eq_instances : universe_instance constraint_function

type !'a puniverses = 'a * universe_instance

val out_punivs : 'a puniverses -> 'a

val in_punivs : 'a -> 'a puniverses

val eq_puniverses : 
  ('a -> 'a -> bool) ->
  'a puniverses ->
  'a puniverses ->
  bool

module UContext : sig ... end

type universe_context = UContext.t

module AUContext : sig ... end

type abstract_universe_context = AUContext.t

module CumulativityInfo : sig ... end

type cumulativity_info = CumulativityInfo.t

module ACumulativityInfo : sig ... end

type abstract_cumulativity_info = ACumulativityInfo.t

module ContextSet : sig ... end

type universe_context_set = ContextSet.t

type !'a in_universe_context = 'a * universe_context

type !'a in_universe_context_set = 'a * universe_context_set

val empty_level_subst : universe_level_subst

val is_empty_level_subst : universe_level_subst -> bool

val subst_univs_level_level : 
  universe_level_subst ->
  universe_level ->
  universe_level

val subst_univs_level_universe : universe_level_subst -> universe -> universe

val subst_univs_level_constraints : 
  universe_level_subst ->
  constraints ->
  constraints

val subst_univs_level_abstract_universe_context : 
  universe_level_subst ->
  abstract_universe_context ->
  abstract_universe_context

val subst_univs_level_instance : 
  universe_level_subst ->
  universe_instance ->
  universe_instance

val empty_subst : universe_subst

val is_empty_subst : universe_subst -> bool

val make_subst : universe_subst -> universe_subst_fn

val subst_univs_universe : universe_subst_fn -> universe -> universe

val subst_univs_constraints : universe_subst_fn -> constraints -> constraints

val subst_instance_instance : 
  universe_instance ->
  universe_instance ->
  universe_instance

val subst_instance_universe : universe_instance -> universe -> universe

val subst_instance_context : 
  universe_instance ->
  abstract_universe_context ->
  universe_context

val make_instance_subst : universe_instance -> universe_level_subst

val make_inverse_instance_subst : universe_instance -> universe_level_subst

val abstract_universes : 
  universe_context ->
  universe_level_subst * abstract_universe_context

val abstract_cumulativity_info : 
  cumulativity_info ->
  universe_level_subst * abstract_cumulativity_info

val make_abstract_instance : abstract_universe_context -> universe_instance

val instantiate_univ_context : abstract_universe_context -> universe_context

val instantiate_cumulativity_info : 
  abstract_cumulativity_info ->
  cumulativity_info

val pr_constraint_type : constraint_type -> Pp.std_ppcmds

val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds

val pr_universe_context : 
  (Level.t -> Pp.std_ppcmds) ->
  universe_context ->
  Pp.std_ppcmds

val pr_cumulativity_info : 
  (Level.t -> Pp.std_ppcmds) ->
  cumulativity_info ->
  Pp.std_ppcmds

val pr_abstract_universe_context : 
  (Level.t -> Pp.std_ppcmds) ->
  abstract_universe_context ->
  Pp.std_ppcmds

val pr_abstract_cumulativity_info : 
  (Level.t -> Pp.std_ppcmds) ->
  abstract_cumulativity_info ->
  Pp.std_ppcmds

val pr_universe_context_set : 
  (Level.t -> Pp.std_ppcmds) ->
  universe_context_set ->
  Pp.std_ppcmds

val explain_universe_inconsistency : 
  (Level.t -> Pp.std_ppcmds) ->
  univ_inconsistency ->
  Pp.std_ppcmds

val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds

val pr_universe_subst : universe_subst -> Pp.std_ppcmds

val hcons_univ : universe -> universe

val hcons_constraints : constraints -> constraints

val hcons_universe_set : universe_set -> universe_set

val hcons_universe_context : universe_context -> universe_context

val hcons_abstract_universe_context : 
  abstract_universe_context ->
  abstract_universe_context

val hcons_universe_context_set : universe_context_set -> universe_context_set

val hcons_cumulativity_info : cumulativity_info -> cumulativity_info

val hcons_abstract_cumulativity_info : 
  abstract_cumulativity_info ->
  abstract_cumulativity_info

val compare_levels : universe_level -> universe_level -> int

val eq_levels : universe_level -> universe_level -> bool

val equal_universes : universe -> universe -> bool

val universes_of_constraints : constraints -> universe_set

package coq