diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2018-03-06 13:41:37 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2018-03-06 19:39:35 +0100 |
| commit | 940b2f972c4b3f42850e36c721564b127d30e496 (patch) | |
| tree | f78dd9dae78e3058a42d862540d5f5cf26a48d31 /plugins/extraction/modutil.mli | |
| parent | 8127e69a678f138ea201ec1251990b1615cb27bc (diff) | |
An experimental 'Show Extraction' command (grant feature wish #4129)
Attempt to extract the current ongoing proof (request by
Clément Pit-Claudel on coqdev, and also #4129).
Evars are handled as axioms.
Diffstat (limited to 'plugins/extraction/modutil.mli')
0 files changed, 0 insertions, 0 deletions