From f9f35dc36f5249a2de18005ab59ae934e0fa7075 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 3 Aug 2009 20:50:11 +0000
Subject: Added "etransitivity". Added support for "injection" and
 "discriminate" on JMeq.

Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.

Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 4c2ed82b8..0688f5246 100644
--- a/CHANGES
+++ b/CHANGES
@@ -24,6 +24,8 @@ Tactics
   variables and "**" for introducing all quantified variables and hypotheses.
 - Pattern Unification for existential variables activated in tactics and 
   new option "Unset Tactic Evars Pattern Unification" to deactivate it.
+- New tactic "etransitivity".
+- Support of JMeq for "injection" and "discriminate".
 
 Tactic Language
 
-- 
cgit v1.2.3