Extract_env (rocq-runtime.Extraction_plugin.Extract

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

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

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

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

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

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

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

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

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