package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type key = int CEphemeron.key option Pervasives.ref
type stratification = {
  1. env_universes : UGraph.t;
  2. env_engagement : Declarations.engagement;
}
type lazy_val
val force_lazy_val : lazy_val -> (Vmvalues.values * Names.Id.Set.t) option
val dummy_lazy_val : unit -> lazy_val
val build_lazy_val : lazy_val -> (Vmvalues.values * Names.Id.Set.t) -> unit
type named_context_val = private {
  1. env_named_ctx : Context.Named.t;
  2. env_named_map : (Context.Named.Declaration.t * lazy_val) Names.Id.Map.t;
}
type rel_context_val = private {
  1. env_rel_ctx : Context.Rel.t;
  2. env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t;
}
type env = {
  1. env_globals : globals;
  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 empty_named_context_val : named_context_val
val empty_env : env
val empty_rel_context_val : rel_context_val
val match_rel_context_val : rel_context_val -> (Context.Rel.Declaration.t * lazy_val * rel_context_val) option
val nb_rel : env -> int
val push_rel : Context.Rel.Declaration.t -> env -> env
val lookup_rel : int -> env -> Context.Rel.Declaration.t
val lookup_rel_val : int -> env -> lazy_val
val env_of_rel : int -> env -> env
val match_named_context_val : named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option
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.t -> env -> constant_key
val lookup_constant : Names.Constant.t -> env -> Declarations.constant_body
val lookup_mind_key : Names.MutInd.t -> env -> mind_key
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct