1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 2040c1b57e..73905ec010 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