package coq
type key = int CEphemeron.key option reftype constant_key = Declarations.constant_body * (link_info ref * key)type mind_key = Declarations.mutual_inductive_body * link_info reftype globals = {env_constants : constant_key Names.Cmap_env.t;env_inductives : mind_key Names.Mindmap_env.t;env_modules : Declarations.module_body Names.MPmap.t;env_modtypes : Declarations.module_type_body Names.MPmap.t;
}val force_lazy_val : lazy_val -> (Term.values * Names.Id.Set.t) optionval dummy_lazy_val : unit -> lazy_valval build_lazy_val : lazy_val -> (Term.values * Names.Id.Set.t) -> unittype named_context_val = private {env_named_ctx : Context.Named.t;env_named_map : (Context.Named.Declaration.t * lazy_val) Names.Id.Map.t;
}type env = {env_globals : globals;env_named_context : named_context_val;env_rel_context : Context.Rel.t;env_rel_val : lazy_val list;env_nb_rel : int;env_stratification : stratification;env_typing_flags : Declarations.typing_flags;env_conv_oracle : Conv_oracle.oracle;retroknowledge : Retroknowledge.retroknowledge;indirect_pterms : Opaqueproof.opaquetab;
}val empty_named_context_val : named_context_valval empty_env : envval nb_rel : env -> intval push_rel : Context.Rel.Declaration.t -> env -> envval push_named_context_val :
Context.Named.Declaration.t ->
named_context_val ->
named_context_valval push_named_context_val_val :
Context.Named.Declaration.t ->
lazy_val ->
named_context_val ->
named_context_valval match_named_context_val :
named_context_val ->
(Context.Named.Declaration.t * lazy_val * named_context_val) optionval map_named_val :
(Term.constr -> Term.constr) ->
named_context_val ->
named_context_valval push_named : Context.Named.Declaration.t -> env -> envval lookup_named : Names.Id.t -> env -> Context.Named.Declaration.tval lookup_named_val : Names.Id.t -> env -> lazy_valval env_of_named : Names.Id.t -> env -> envval lookup_constant_key : Names.constant -> env -> constant_keyval lookup_constant : Names.constant -> env -> Declarations.constant_bodyval lookup_mind_key : Names.mutual_inductive -> env -> mind_keyval lookup_mind :
Names.mutual_inductive ->
env ->
Declarations.mutual_inductive_body