coq 8.7.2 · OCaml Package

type env

val pre_env : env -> Pre_env.env

val env_of_pre_env : Pre_env.env -> env

val oracle : env -> Conv_oracle.oracle

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

type named_context_val

val eq_named_context_val : named_context_val -> named_context_val -> bool

val empty_env : env

val universes : env -> UGraph.t

val rel_context : env -> Context.Rel.t

val named_context : env -> Context.Named.t

val named_context_val : env -> named_context_val

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 empty_context : env -> bool

val nb_rel : env -> int

val push_rel : Context.Rel.Declaration.t -> env -> env

val push_rel_context : Context.Rel.t -> env -> env

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

val lookup_rel : int -> env -> Context.Rel.Declaration.t

val evaluable_rel : int -> env -> bool

val fold_rel_context : 
  (env -> Context.Rel.Declaration.t -> 'a -> 'a) ->
  env ->
  init:'a ->
  'a

val named_context_of_val : named_context_val -> Context.Named.t

val val_of_named_context : Context.Named.t -> named_context_val

val empty_named_context_val : named_context_val

val map_named_val : 
  (Term.constr -> Term.constr) ->
  named_context_val ->
  named_context_val

val push_named : Context.Named.Declaration.t -> env -> env

val push_named_context : Context.Named.t -> env -> env

val push_named_context_val : 
  Context.Named.Declaration.t ->
  named_context_val ->
  named_context_val

val lookup_named : Names.variable -> env -> Context.Named.Declaration.t

val lookup_named_val : 
  Names.variable ->
  named_context_val ->
  Context.Named.Declaration.t

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

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

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

val fold_named_context : 
  (env -> Context.Named.Declaration.t -> 'a -> 'a) ->
  env ->
  init:'a ->
  'a

val fold_named_context_reverse : 
  ('a -> Context.Named.Declaration.t -> '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 add_constant : Names.constant -> Declarations.constant_body -> env -> env

val add_constant_key : 
  Names.constant ->
  Declarations.constant_body ->
  Pre_env.link_info ->
  env ->
  env

val lookup_constant : Names.constant -> env -> Declarations.constant_body

val evaluable_constant : Names.constant -> env -> bool

val polymorphic_constant : Names.constant -> env -> bool

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

val type_in_type_constant : Names.constant -> env -> bool

val template_polymorphic_constant : Names.constant -> env -> bool

val template_polymorphic_pconstant : Term.pconstant -> env -> bool

type const_evaluation_result =

| NoBody
| Opaque
| IsProj

exception NotEvaluableConst of const_evaluation_result

val constant_value : 
  env ->
  Names.constant Univ.puniverses ->
  Term.constr Univ.constrained

val constant_type : 
  env ->
  Names.constant Univ.puniverses ->
  Declarations.constant_type Univ.constrained

val constant_opt_value : 
  env ->
  Names.constant Univ.puniverses ->
  (Term.constr * Univ.constraints) option

val constant_value_and_type : 
  env ->
  Names.constant Univ.puniverses ->
  Term.constr option * Declarations.constant_type * Univ.constraints

val constant_context : env -> Names.constant -> Univ.universe_context

val constant_instance : env -> Names.constant -> Univ.universe_instance

val constant_value_in : env -> Names.constant Univ.puniverses -> Term.constr

val constant_type_in : 
  env ->
  Names.constant Univ.puniverses ->
  Declarations.constant_type

val constant_opt_value_in : 
  env ->
  Names.constant Univ.puniverses ->
  Term.constr option

val lookup_projection : Names.projection -> env -> Declarations.projection_body

val is_projection : Names.constant -> env -> bool

val add_mind_key : Names.mutual_inductive -> Pre_env.mind_key -> env -> env

val add_mind : 
  Names.mutual_inductive ->
  Declarations.mutual_inductive_body ->
  env ->
  env

val lookup_mind : 
  Names.mutual_inductive ->
  env ->
  Declarations.mutual_inductive_body

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

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

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

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

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

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

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

val lookup_module : Names.module_path -> env -> Declarations.module_body

val lookup_modtype : Names.module_path -> env -> Declarations.module_type_body

val add_constraints : Univ.constraints -> env -> env

val check_constraints : Univ.constraints -> env -> bool

val push_context : ?strict:bool -> Univ.universe_context -> env -> env

val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env

val push_constraints_to_env : 'a Univ.constrained -> env -> env

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

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

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

val vars_of_global : env -> Term.constr -> Names.Id.Set.t

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

val keep_hyps : env -> Names.Id.Set.t -> Context.Named.t

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

uj_val : 'constr;
uj_type : 'types;

}

type unsafe_judgment = (Term.constr, Term.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 : Term.sorts;

}

type unsafe_type_judgment = Term.types punsafe_type_judgment

val compile_constant_body : 
  env ->
  Declarations.constant_universes ->
  Declarations.constant_def ->
  Cemitcodes.body_code option

exception Hyp_not_found

val apply_to_hyp : 
  named_context_val ->
  Names.variable ->
  (Context.Named.t ->
    Context.Named.Declaration.t ->
    Context.Named.t ->
    Context.Named.Declaration.t) ->
  named_context_val

val remove_hyps : 
  Names.Id.Set.t ->
  (Context.Named.Declaration.t -> Context.Named.Declaration.t) ->
  (Pre_env.lazy_val -> Pre_env.lazy_val) ->
  named_context_val ->
  named_context_val

val retroknowledge : (Retroknowledge.retroknowledge -> 'a) -> env -> 'a

val registered : env -> Retroknowledge.field -> bool

val register : env -> Retroknowledge.field -> Retroknowledge.entry -> env

val no_link_info : Pre_env.link_info

package coq