Extract_env (u.3758aa3ddc38cffa23da0eeb3fa7893a.rocq-runtime.9.0.0.doc.extraction_plugin.Extraction_plugin.Extract

Source

val simple_extraction : 
  opaque_access:Global.indirect_accessor ->
  Libnames.qualid ->
  unit

Source

val full_extraction : 
  opaque_access:Global.indirect_accessor ->
  string option ->
  Libnames.qualid list ->
  unit

Source

val separate_extraction : 
  opaque_access:Global.indirect_accessor ->
  Libnames.qualid list ->
  unit

Source

val extraction_library : 
  opaque_access:Global.indirect_accessor ->
  bool ->
  Names.lident ->
  unit

Source

val extract_and_compile : 
  opaque_access:Global.indirect_accessor ->
  Libnames.qualid list ->
  unit

Source

val mono_environment : 
  opaque_access:Global.indirect_accessor ->
  Names.GlobRef.t list ->
  Names.ModPath.t list ->
  Miniml.ml_structure

Source

val print_one_decl : 
  Miniml.ml_structure ->
  Names.ModPath.t ->
  Miniml.ml_decl ->
  Pp.t

Source

val structure_for_compute : 
  opaque_access:Global.indirect_accessor ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.t ->
  Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type

Sourceval show_extraction : pstate:Declare.Proof.t -> unit