From b0b98c1a236fca450a183ecae5157ed70e3da6c6 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 3 Oct 2002 15:45:01 +0000
Subject: Intégration des modifs de la V7.3.1
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index f7a71e2bf..16f9a9db5 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,4 +1,4 @@
-Changes from V7.3 to ????
+Changes from V7.3.1 to ????
 -------------------------
 
 Library
@@ -61,6 +61,24 @@ Incompatibilities
   proofs; in some cases, incompatibilites is solved by declaring locally 
   opaque the relevant constant)
 
+Changes from V7.3 to V7.3.1
+===========================
+
+Bug fixes
+
+  - Corrupted Field tactic and Match Context tactic construction fixed
+  - Checking of names already existing in Assert added (PR#182)
+  - Invalid argument bug in Exact tactic solved (PR#183)
+  - Colliding bound names bug fixed (PR#202)
+  - Wrong non-recursivity test for Record fixed (PR#189)
+  - Out of memory/seg fault bug related to parametric inductive fixed (PR#195)
+  - Setoid_replace/Setoid_rewrite bug wrt "==" fixed
+
+Misc
+
+  - Ocaml version >= 3.06 is needed to compile Coq from sources
+  - Simplification of fresh names creation strategy for Assert, Pose and 
+    LetTac (PR#192)
 
 Changes from V7.2 to V7.3
 -------------------------
-- 
cgit v1.2.3