From 6679d01256ce9a4a05c13eabbb4e2d85c3e6f075 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2012 21:08:39 +0000
Subject: 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
---
 CHANGES | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'CHANGES')

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
 
-- 
cgit v1.2.3