Internal (p.rocq-runtime.9.2.0.doc.rocq-runtime.kernel.Environ.Internal)

Sourceval push_template_context : UVars.UContext.t -> env -> env

Makes the qvars treated as above prop. Do not use outside kernel inductive typechecking.

Sourceval is_above_prop : env -> Sorts.QVar.t -> bool

Sourcemodule View : sig ... end

View type only used by Serlib. Do not use otherwise.

val shallow_overwrite_module : 
  Names.ModPath.t ->
  Mod_declarations.module_body ->
  env ->
  env

Same as shallow_add_module but tolerates that the module is already in the environment. Only used to bypass a dubious implementation in extraction, do not use.

Source

val overwrite_module : 
  Names.ModPath.t ->
  Mod_declarations.module_body ->
  env ->
  env

Overwriting variant of Modops.add_module, see above.

Source

val overwrite_module_parameter : 
  Names.MBId.t ->
  Mod_declarations.module_type_body ->
  env ->
  env

Overwriting variant of Modops.add_module_parameter, see above.

Source

val overwrite_structure : 
  Names.ModPath.t ->
  Mod_declarations.structure_body ->
  Mod_subst.delta_resolver ->
  env ->
  env

Overwriting variant of Modops.add_structure, see above.