1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2b10aad68..51b812a20 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,8 @@ Vernacular Commands
 - For the Extraction Language command, "OCaml" is spelled correctly.
   The older "Ocaml" is still accepted, but deprecated.
 - Using “Require” inside a section is deprecated.
+- An experimental command "Show Extraction" allows to extract the content
+  of the current ongoing proof (grant wish #4129).
 
 Universes