diff options
| author | Pierre Letouzey | 2018-03-06 11:53:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2018-03-06 19:38:53 +0100 |
| commit | 8127e69a678f138ea201ec1251990b1615cb27bc (patch) | |
| tree | bd6e011f288f58e711944186acc75e6dd57f91f6 /plugins/extraction/extraction.mli | |
| parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (diff) | |
Extraction: switch to EConstr.t as the central type to extract from.
This is a bit artificial since the extraction normally operates on
finished constrs (with no evars). But:
- Since we use Retyping quite a lot, switching to EConstr.t allows
to get rid of many `EConstr.Unsafe.to_constr (... (EConstr.of_constr ...))`
- This prepares the way for a possible extraction of the content
of ongoing proofs (a forthcoming `Show Extraction` command, see #4129 )
Diffstat (limited to 'plugins/extraction/extraction.mli')
| -rw-r--r-- | plugins/extraction/extraction.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index b15b88ed2c..3a4ba0b34d 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -9,9 +9,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 @@ -20,16 +20,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 *) -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 ? *) |