Extraction_plugin.ExtractionSourceval extract_constant :
Environ.env ->
Names.Constant.t ->
Declarations.constant_body ->
Miniml.ml_declval extract_constant_spec :
Environ.env ->
Names.Constant.t ->
'a Declarations.pconstant_body ->
Miniml.ml_specFor extracting "module ... with ..." declaration
val extract_with_type :
Environ.env ->
Evd.evar_map ->
EConstr.t ->
(Names.Id.t list * Miniml.ml_type) optionval extract_fixpoint :
Environ.env ->
Evd.evar_map ->
Names.Constant.t array ->
(EConstr.t, EConstr.types) Constr.prec_declaration ->
Miniml.ml_declFor Extraction Compute and Show Extraction
val extract_constr :
Environ.env ->
Evd.evar_map ->
EConstr.t ->
Miniml.ml_ast * Miniml.ml_type