coq 8.13.1 · OCaml Package

type lazy_val

val build_lazy_val : lazy_val -> (Vmvalues.values * Names.Id.Set.t) -> unit

val force_lazy_val : lazy_val -> (Vmvalues.values * Names.Id.Set.t) option

val dummy_lazy_val : unit -> lazy_val

type link_info =

| Linked of string
| NotLinked

type key = int CEphemeron.key option Stdlib.ref

type constant_key =
  Opaqueproof.opaque Declarations.constant_body * (link_info Stdlib.ref * key)

type mind_key = Declarations.mutual_inductive_body * link_info Stdlib.ref

module Globals : sig ... end

type stratification = {

env_universes : UGraph.t;
env_sprop_allowed : bool;
env_universes_lbound : UGraph.Bound.t;
env_engagement : Declarations.engagement;

}

type named_context_val = private {

env_named_ctx : Constr.named_context;
env_named_map : (Constr.named_declaration * lazy_val) Names.Id.Map.t;
env_named_var : Constr.t list;

}

type rel_context_val = private {

env_rel_ctx : Constr.rel_context;
env_rel_map : (Constr.rel_declaration * lazy_val) Range.t;

}

type env = private {

env_globals : Globals.t;
env_named_context : named_context_val;
env_rel_context : rel_context_val;
env_nb_rel : int;
env_stratification : stratification;
env_typing_flags : Declarations.typing_flags;
retroknowledge : Retroknowledge.retroknowledge;
indirect_pterms : Opaqueproof.opaquetab;

}

val oracle : env -> Conv_oracle.oracle

val set_oracle : env -> Conv_oracle.oracle -> env

val eq_named_context_val : named_context_val -> named_context_val -> bool

val empty_env : env

val universes : env -> UGraph.t

val universes_lbound : env -> UGraph.Bound.t

val set_universes_lbound : env -> UGraph.Bound.t -> env

val rel_context : env -> Constr.rel_context

val named_context : env -> Constr.named_context

val named_context_val : env -> named_context_val

val set_universes : UGraph.t -> env -> env

val opaque_tables : env -> Opaqueproof.opaquetab

val set_opaque_tables : env -> Opaqueproof.opaquetab -> env

val engagement : env -> Declarations.engagement

val typing_flags : env -> Declarations.typing_flags

val is_impredicative_set : env -> bool

val type_in_type : env -> bool

val deactivated_guard : env -> bool

val indices_matter : env -> bool

val is_impredicative_sort : env -> Sorts.t -> bool

val is_impredicative_univ : env -> Univ.Universe.t -> bool

val is_impredicative_family : env -> Sorts.family -> bool

val empty_context : env -> bool

val nb_rel : env -> int

val push_rel : Constr.rel_declaration -> env -> env

val push_rel_context : Constr.rel_context -> env -> env

val push_rec_types : Constr.rec_declaration -> env -> env

val lookup_rel : int -> env -> Constr.rel_declaration

val lookup_rel_val : int -> env -> lazy_val

val evaluable_rel : int -> env -> bool

val env_of_rel : int -> env -> env

val fold_rel_context : 
  (env -> Constr.rel_declaration -> 'a -> 'a) ->
  env ->
  init:'a ->
  'a

val named_context_of_val : named_context_val -> Constr.named_context

val val_of_named_context : Constr.named_context -> named_context_val

val empty_named_context_val : named_context_val

val ids_of_named_context_val : named_context_val -> Names.Id.Set.t

val map_named_val : 
  (Constr.named_declaration -> Constr.named_declaration) ->
  named_context_val ->
  named_context_val

val push_named : Constr.named_declaration -> env -> env

val push_named_context : Constr.named_context -> env -> env

val push_named_context_val : 
  Constr.named_declaration ->
  named_context_val ->
  named_context_val

val lookup_named : Names.variable -> env -> Constr.named_declaration

val lookup_named_val : Names.variable -> env -> lazy_val

val lookup_named_ctxt : 
  Names.variable ->
  named_context_val ->
  Constr.named_declaration

val evaluable_named : Names.variable -> env -> bool

val named_type : Names.variable -> env -> Constr.types

val named_body : Names.variable -> env -> Constr.constr option

val fold_named_context : 
  (env -> Constr.named_declaration -> 'a -> 'a) ->
  env ->
  init:'a ->
  'a

val match_named_context_val : 
  named_context_val ->
  (Constr.named_declaration * lazy_val * named_context_val) option

val fold_named_context_reverse : 
  ('a -> Constr.named_declaration -> 'a) ->
  init:'a ->
  env ->
  'a

val reset_context : env -> env

val reset_with_named_context : named_context_val -> env -> env

val pop_rel_context : int -> env -> env

val fold_constants : 
  (Names.Constant.t ->
    Opaqueproof.opaque Declarations.constant_body ->
    'a ->
    'a) ->
  env ->
  'a ->
  'a

val fold_inductives : 
  (Names.MutInd.t -> Declarations.mutual_inductive_body -> 'a -> 'a) ->
  env ->
  'a ->
  'a

val add_constant : 
  Names.Constant.t ->
  Opaqueproof.opaque Declarations.constant_body ->
  env ->
  env

val add_constant_key : 
  Names.Constant.t ->
  Opaqueproof.opaque Declarations.constant_body ->
  link_info ->
  env ->
  env

val lookup_constant_key : Names.Constant.t -> env -> constant_key

val lookup_constant : 
  Names.Constant.t ->
  env ->
  Opaqueproof.opaque Declarations.constant_body

val evaluable_constant : Names.Constant.t -> env -> bool

val mem_constant : Names.Constant.t -> env -> bool

val polymorphic_constant : Names.Constant.t -> env -> bool

val polymorphic_pconstant : Constr.pconstant -> env -> bool

val type_in_type_constant : Names.Constant.t -> env -> bool

type const_evaluation_result =

| NoBody
| Opaque
| IsPrimitive of Univ.Instance.t * CPrimitives.t

exception NotEvaluableConst of const_evaluation_result

val constant_type : 
  env ->
  Names.Constant.t Univ.puniverses ->
  Constr.types Univ.constrained

val constant_value_and_type : 
  env ->
  Names.Constant.t Univ.puniverses ->
  Constr.constr option * Constr.types * Univ.Constraint.t

val constant_context : env -> Names.Constant.t -> Univ.AUContext.t

val constant_value_in : 
  env ->
  Names.Constant.t Univ.puniverses ->
  Constr.constr

val constant_type_in : env -> Names.Constant.t Univ.puniverses -> Constr.types

val constant_opt_value_in : 
  env ->
  Names.Constant.t Univ.puniverses ->
  Constr.constr option

val is_primitive : env -> Names.Constant.t -> bool

val is_array_type : env -> Names.Constant.t -> bool

val lookup_projection : Names.Projection.t -> env -> Constr.types

val get_projection : 
  env ->
  Names.inductive ->
  proj_arg:int ->
  Names.Projection.Repr.t option

val get_projections : 
  env ->
  Names.inductive ->
  Names.Projection.Repr.t array option

val lookup_mind_key : Names.MutInd.t -> env -> mind_key

val add_mind_key : Names.MutInd.t -> mind_key -> env -> env

val add_mind : 
  Names.MutInd.t ->
  Declarations.mutual_inductive_body ->
  env ->
  env

val lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body

val mem_mind : Names.MutInd.t -> env -> bool

val mind_context : env -> Names.MutInd.t -> Univ.AUContext.t

val polymorphic_ind : Names.inductive -> env -> bool

val polymorphic_pind : Constr.pinductive -> env -> bool

val type_in_type_ind : Names.inductive -> env -> bool

val template_polymorphic_ind : Names.inductive -> env -> bool

val template_polymorphic_variables : 
  Names.inductive ->
  env ->
  Univ.Level.t list

val template_polymorphic_pind : Constr.pinductive -> env -> bool

module type QNameS = sig ... end

module QConstant : sig ... end

module QMutInd : sig ... end

module QInd : sig ... end

module QConstruct : sig ... end

module QProjection : sig ... end

module QGlobRef : sig ... end

val add_modtype : Declarations.module_type_body -> env -> env

val shallow_add_module : Declarations.module_body -> env -> env

val lookup_module : Names.ModPath.t -> env -> Declarations.module_body

val lookup_modtype : Names.ModPath.t -> env -> Declarations.module_type_body

val add_constraints : Univ.Constraint.t -> env -> env

val check_constraints : Univ.Constraint.t -> env -> bool

val push_context : ?strict:bool -> Univ.UContext.t -> env -> env

val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env

val push_subgraph : Univ.ContextSet.t -> env -> env

val set_engagement : Declarations.engagement -> env -> env

val set_typing_flags : Declarations.typing_flags -> env -> env

val set_cumulative_sprop : bool -> env -> env

val set_type_in_type : bool -> env -> env

val set_allow_sprop : bool -> env -> env

val sprop_allowed : env -> bool

val update_typing_flags : ?typing_flags:Declarations.typing_flags -> env -> env

val universes_of_global : env -> Names.GlobRef.t -> Univ.AUContext.t

val global_vars_set : env -> Constr.constr -> Names.Id.Set.t

val vars_of_global : env -> Names.GlobRef.t -> Names.Id.Set.t

val really_needed : env -> Names.Id.Set.t -> Names.Id.Set.t

val keep_hyps : env -> Names.Id.Set.t -> Constr.named_context

type (!'constr, !'types) punsafe_judgment = {

uj_val : 'constr;
uj_type : 'types;

}

val on_judgment : 
  ('a -> 'b) ->
  ('a, 'a) punsafe_judgment ->
  ('b, 'b) punsafe_judgment

val on_judgment_value : 
  ('c -> 'c) ->
  ('c, 't) punsafe_judgment ->
  ('c, 't) punsafe_judgment

val on_judgment_type : 
  ('t -> 't) ->
  ('c, 't) punsafe_judgment ->
  ('c, 't) punsafe_judgment

type unsafe_judgment = (Constr.constr, Constr.types) punsafe_judgment

val make_judge : 'constr -> 'types -> ('constr, 'types) punsafe_judgment

val j_val : ('constr, 'types) punsafe_judgment -> 'constr

val j_type : ('constr, 'types) punsafe_judgment -> 'types

type !'types punsafe_type_judgment = {

utj_val : 'types;
utj_type : Sorts.t;

}

type unsafe_type_judgment = Constr.types punsafe_type_judgment

exception Hyp_not_found

val apply_to_hyp : 
  named_context_val ->
  Names.variable ->
  (Constr.named_context ->
    Constr.named_declaration ->
    Constr.named_context ->
    Constr.named_declaration) ->
  named_context_val

val remove_hyps : 
  Names.Id.Set.t ->
  (Constr.named_declaration -> Constr.named_declaration) ->
  (lazy_val -> lazy_val) ->
  named_context_val ->
  named_context_val

val is_polymorphic : env -> Names.GlobRef.t -> bool

val is_template_polymorphic : env -> Names.GlobRef.t -> bool

val get_template_polymorphic_variables : 
  env ->
  Names.GlobRef.t ->
  Univ.Level.t list

val is_type_in_type : env -> Names.GlobRef.t -> bool

val no_link_info : link_info

val set_retroknowledge : env -> Retroknowledge.retroknowledge -> env

package coq