From be01deca2b8ff22505adaa66f55f005673bf2d85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 May 2014 15:06:46 +0200
Subject: More on injection over a projectable "existT". - Fixing syntax
 "injection ... as ..." which was not working. - Now applying the
 simplification on any "existT" generated by "injection" (possible source of
 incompatibilities).

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 66d5a0e0f7..a3c8bf6f05 100644
--- a/CHANGES
+++ b/CHANGES
@@ -102,6 +102,10 @@ Tactics
   independently of the number of ipats, which has itself to be less
   than the number of new hypotheses (possible source of incompatibilities;
   former behavior obtainable by "Unset Injection L2R Pattern Order").
+- Tactic "injection" now automatically simplifies subgoals
+  "existT n p = exists n p'" into "p = p'" when "n" is in an inductive type for
+  which a decidable equality scheme has been generated with "Scheme Equality"
+  (possible source of incompatibilities).
 - New tactic "rewrite_strat" for generalized rewriting with user-defined
   strategies, subsumming autorewrite.
 - Injection can now also deduce equality of arguments of sort Prop, by using
-- 
cgit v1.2.3