coq 8.7.1 · OCaml Package

type link_info =

type key = int CEphemeron.key option ref

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

type mind_key = Declarations.mutual_inductive_body * link_info ref

type globals = {

}

type stratification = {

}

type lazy_val

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

val dummy_lazy_val : unit -> lazy_val

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

type named_context_val = private {

}

type env = {

}

val empty_named_context_val : named_context_val

val empty_env : env

val nb_rel : env -> int

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

val lookup_rel_val : int -> env -> lazy_val

val env_of_rel : int -> env -> env

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

val push_named_context_val_val : 
  Context.Named.Declaration.t ->
  lazy_val ->
  named_context_val ->
  named_context_val

val match_named_context_val : 
  named_context_val ->
  (Context.Named.Declaration.t * lazy_val * named_context_val) option

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

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

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

val lookup_named_val : Names.Id.t -> env -> lazy_val

val env_of_named : Names.Id.t -> env -> env

val lookup_constant_key : Names.constant -> env -> constant_key

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

val lookup_mind_key : Names.mutual_inductive -> env -> mind_key

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

package coq