Module `Extraction_plugin.Extract_env`

val simple_extraction : Libnames.qualid -> unit
val full_extraction : string option -> Libnames.qualid list -> unit
val separate_extraction : Libnames.qualid list -> unit
val extraction_library : bool -> Names.Id.t -> unit
val extract_and_compile : Libnames.qualid list -> unit
val mono_environment : 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 : Environ.env -> Evd.evar_map -> EConstr.t -> Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type
val show_extraction : pstate:Proof_global.t -> unit