diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:24:04 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:24:04 +0100 |
| commit | 374d1efc5de20f8c99c13a7216357a7228c353e8 (patch) | |
| tree | 57c77f168c5b5e0d8164128d7977e2bd0efdfc7f /plugins/extraction/extraction.mli | |
| parent | a40fb961c8ffeeb03769404cacda8bd6cff17417 (diff) | |
| parent | 940b2f972c4b3f42850e36c721564b127d30e496 (diff) | |
Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish #4129)
Diffstat (limited to 'plugins/extraction/extraction.mli')
| -rw-r--r-- | plugins/extraction/extraction.mli | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index a0f2885a4..d27c79cb6 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -11,9 +11,9 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Constr open Declarations open Environ +open Evd open Miniml val extract_constant : env -> Constant.t -> constant_body -> ml_decl @@ -22,16 +22,18 @@ val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) -val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option +val extract_with_type : + env -> evar_map -> EConstr.t -> ( Id.t list * ml_type ) option val extract_fixpoint : - env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl + env -> evar_map -> Constant.t array -> + (EConstr.t, EConstr.types) Constr.prec_declaration -> ml_decl val extract_inductive : env -> MutInd.t -> ml_ind -(** For extraction compute *) +(** For Extraction Compute and Show Extraction *) -val extract_constr : env -> constr -> ml_ast * ml_type +val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type (*s Is a [ml_decl] or a [ml_spec] logical ? *) |