1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index d6e92a9bf..e03ab683c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -39,6 +39,8 @@ Vernacular Commands
 
 - The deprecated Coercion Local, Open Local Scope, Notation Local syntax
   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.
 
 Universes