package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 key = int CEphemeron.key option ref
module Globals : sig ... end
type stratification = {
  1. env_universes : UGraph.t;
  2. env_sprop_allowed : bool;
  3. env_universes_lbound : UGraph.Bound.t;
  4. env_engagement : Declarations.engagement;
}
type named_context_val = private {
  1. env_named_ctx : Constr.named_context;
  2. env_named_map : (Constr.named_declaration * lazy_val) Names.Id.Map.t;
  3. env_named_var : Constr.t list;
}
type rel_context_val = private {
  1. env_rel_ctx : Constr.rel_context;
  2. env_rel_map : (Constr.rel_declaration * lazy_val) Range.t;
}
type env = private {
  1. env_globals : Globals.t;
  2. env_named_context : named_context_val;
  3. env_rel_context : rel_context_val;
  4. env_nb_rel : int;
  5. env_stratification : stratification;
  6. env_typing_flags : Declarations.typing_flags;
  7. retroknowledge : Retroknowledge.retroknowledge;
  8. 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 push_named : Constr.named_declaration -> env -> env
val push_named_context : Constr.named_context -> env -> env
val lookup_named_val : Names.variable -> env -> lazy_val
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 lookup_constant_key : Names.Constant.t -> env -> constant_key
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 =
  1. | NoBody
  2. | Opaque
  3. | IsPrimitive of Univ.Instance.t * CPrimitives.t
exception NotEvaluableConst of const_evaluation_result
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 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 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
type (!'constr, !'types) punsafe_judgment = {
  1. uj_val : 'constr;
  2. 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 = {
  1. utj_val : 'types;
  2. utj_type : Sorts.t;
}
type unsafe_type_judgment = Constr.types punsafe_type_judgment
exception Hyp_not_found
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 set_retroknowledge : env -> Retroknowledge.retroknowledge -> env