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/extract_env.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/extract_env.mli')
| -rw-r--r-- | plugins/extraction/extract_env.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index dd86177381..196fa08ee5 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -34,4 +34,5 @@ val print_one_decl : (* Used by Extraction Compute *) val structure_for_compute : - Constr.t -> (Miniml.ml_decl list) * Miniml.ml_ast * Miniml.ml_type + Environ.env -> Evd.evar_map -> EConstr.t -> + Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type |