aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/g_extraction.ml4
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2018-03-06 11:53:59 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2018-03-06 19:38:53 +0100
commit8127e69a678f138ea201ec1251990b1615cb27bc (patch)
treebd6e011f288f58e711944186acc75e6dd57f91f6 /plugins/extraction/g_extraction.ml4
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (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/g_extraction.ml4')
0 files changed, 0 insertions, 0 deletions