diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2018-03-06 11:53:59 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2018-03-06 19:38:53 +0100 |
| commit | 8127e69a678f138ea201ec1251990b1615cb27bc (patch) | |
| tree | bd6e011f288f58e711944186acc75e6dd57f91f6 /interp/notation.ml | |
| 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 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions