Added new command "Set Parsing Explicit" for deactivating parsing (and

printing) of implicit arguments (a priori useful for teaching).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 1334aa739f..cadfec6b89 100644
--- a/CHANGES
+++ b/CHANGES
@@ -5,8 +5,16 @@ Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
 
-Changes from V8.3 to V8.4
-=========================
+Changes from V8.4beta to V8.4
+=============================
+
+Vernacular commands
+
+- New command "Set Parsing Explicit" for deactivating parsing (and printing)
+  of implicit arguments (useful for teaching).
+
+Changes from V8.3 to V8.4beta
+=============================
 
 Logic