package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.3.0.tar.gz
sha256=3f0fc283e8644394aa9c7a6e3995b6d9ebbe1e6dda712bf431f9c372dcef95ad
doc/rocq-runtime.kernel/Environ/Internal/View/index.html
Module Internal.ViewSource
View type only used by Serlib. Do not use otherwise.
Source
type t = {env_constants : Declarations.constant_body Names.Cmap_env.t;env_inductives : Declarations.mutual_inductive_body Names.Mindmap_env.t;env_modules : Mod_declarations.module_body Names.ModPath.Map.t;env_modtypes : Mod_declarations.module_type_body Names.ModPath.Map.t;env_named_context : Constr.named_context;env_rel_context : Constr.rel_context;env_universes : UGraph.t;env_qualities : Sorts.Quality.Set.t;env_symb_pats : Declarations.machine_rewrite_rule list Names.Cmap_env.t;env_typing_flags : Declarations.typing_flags;
}