aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2018-03-06 13:41:37 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2018-03-06 19:39:35 +0100
commit940b2f972c4b3f42850e36c721564b127d30e496 (patch)
treef78dd9dae78e3058a42d862540d5f5cf26a48d31 /CHANGES
parent8127e69a678f138ea201ec1251990b1615cb27bc (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 'CHANGES')
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2040c1b57..73905ec01 100644
--- a/CHANGES
+++ b/CHANGES
@@ -70,6 +70,8 @@ Vernacular Commands
was removed. Use Local as a prefix instead.
- For the Extraction Language command, "OCaml" is spelled correctly.
The older "Ocaml" is still accepted, but deprecated.
+- An experimental command "Show Extraction" allows to extract the content
+ of the current ongoing proof (grant wish #4129).
Universes