Up – Package index » rocq-runtime » Library rocq-runtime.checklib » Coq_checklib » Safe_checking

Module `Coq_checklib.Safe_checking`Source

val import : 
  Safe_typing.safe_environment ->
  Names.Cset.t Names.Cmap.t ->
  Safe_typing.compiled_library ->
  Vmlibrary.on_disk ->
  Safe_typing.vodigest ->
  Safe_typing.safe_environment * Names.Cset.t Names.Cmap.t

Source

val unsafe_import : 
  Safe_typing.safe_environment ->
  Safe_typing.compiled_library ->
  Vmlibrary.on_disk ->
  Safe_typing.vodigest ->
  Safe_typing.safe_environment