diff options
| author | Pierre Letouzey | 2018-03-06 13:41:37 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2018-03-06 19:39:35 +0100 |
| commit | 940b2f972c4b3f42850e36c721564b127d30e496 (patch) | |
| tree | f78dd9dae78e3058a42d862540d5f5cf26a48d31 /plugins/extraction/extraction.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/extraction.mli')
| -rw-r--r-- | plugins/extraction/extraction.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 3a4ba0b34d..ec39a2eae8 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -29,7 +29,7 @@ val extract_fixpoint : val extract_inductive : env -> MutInd.t -> ml_ind -(** For extraction compute *) +(** For Extraction Compute and Show Extraction *) val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type |