From 6eede071cb97e1e39772c2bdecb5189c4fa2adb0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Jan 2016 23:28:40 +0100
Subject: Extending "contradiction" so that it recognizes statements such as
 "~x=x" or ~True.

Found 1 incompatibility in tested contribs and 3 times the same
pattern of incompatibility in the standard library. In all cases, it
is an improvement in the form of the script.

New behavior deactivated when version is <= 8.5.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 594bbc8316..f7e1dee4c7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -61,6 +61,10 @@ Tactics
   "Structural Injection". In this case, hypotheses are also put in the
   context in the natural left-to-right order and the hypothesis on
   which injection applies is cleared.
+- Tactic "contradiction" (hence "easy") now also solve goals with
+  hypotheses of the form "~True" or "t<>t" (possible source of
+  incompatibilities because of more successes in automation, but
+  generally a more intuitive strategy).
 
 Hints
 
-- 
cgit v1.2.3


From 530287b4cd26b10457cad95dd6b41592e21ef440 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 21 Sep 2016 10:48:20 +0200
Subject: Fix description of change in intro semantics.

---
 CHANGES | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index f7e1dee4c7..c3eaae6ee0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -50,9 +50,10 @@ Tactics
 - Every generic argument type declares a tactic scope of the form "name:(...)"
   where name is the name of the argument. This generalizes the constr: and ltac:
   instances.
-- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use
-  a locally free identifier anymore. It must use e.g. the "fresh" primitive
-  instead (potential source of incompatibilities).
+- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is
+  given a free identifier, it is not bound in subsequent tactics anymore.
+  In order to introduce a binding, use e.g. the "fresh" primitive instead
+  (potential source of incompatibilities).
 - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
 - New goal selectors.  Sets of goals can be selected by select by listing
   integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24.
-- 
cgit v1.2.3