From 7ac5be3b1e433c028b55c44f0ddfe805634ff0f1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 Aug 2012 17:45:06 +0000
Subject: Some changes in CHANGES.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15730 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/CHANGES b/CHANGES
index 8ac05fb04a..8f3c3eb894 100644
--- a/CHANGES
+++ b/CHANGES
@@ -12,19 +12,20 @@ Vernacular commands
 Specification Language
 
 - The syntax "x -> y" is now declared at level 99. In particular, it has
-  now a lower priority than "<->" : "A -> B <-> C" is now "A -> (B <-> C)".
+  now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
+  (possible source of incompatibilities)
 
 Tactics
 
 - Tactics btauto, a reflexive boolean tautology solver.
 - Tactic "tauto" was exceptionally able to destruct other connectives
-  than the binary connectives "and", "or", "prod", "sum", "iff".  This
+  than the binary connectives "and", "or", "prod", "sum", "iff". This
   non-uniform behavior has been fixed (bug #2680) and tauto is
-  slightly weaker. On the opposite side, new tactic "dtauto" is able
-  to destruct any record-like inductive types, superseding the old
-  version of "tauto".
+  slightly weaker (possible source of incompatibilities). On the
+  opposite side, new tactic "dtauto" is able to destruct any
+  record-like inductive types, superseding the old version of "tauto".
 - Similarly, "intuition" has been made more uniform and, where it now
-  fails, "dintuition" can be used.
+  fails, "dintuition" can be used. (possible source of incompatibilities)
 
 Program
 
@@ -186,7 +187,7 @@ Tactics
 - Using "auto with nocore" disables the use of the "core" database (wish #2188).
   This pseudo-database "nocore" can also be used with trivial and eauto.
 - Tactics "set", "destruct" and "induction" accepts incomplete terms and
-  use the goal to complete the pattern assuming it is no ambiguous.
+  use the goal to complete the pattern assuming it is non ambiguous.
 - When used on arguments with a dependent type, tactics such as
   "destruct", "induction", "case", "elim", etc. now try to abstract
   automatically the dependencies over the arguments of the types
-- 
cgit v1.2.3