From 450ea7ae18da2dc0efc6ac2aed7dee060ed4692a Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 17 Jan 2003 15:19:41 +0000
Subject: Mise a jour pour distrib

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

diff --git a/CHANGES b/CHANGES
index c0ec7c8df0..21bff14073 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,5 @@
 Changes from V7.3.1 to V7.4
--------------------------
+---------------------------
 
 Grammar extension
 
@@ -35,9 +35,12 @@ Library
   unrealistic cases).
 - More efficient versions of Zmult and times (30% faster)
 
+Modules
+
+- Beta version, see doc chap 2.5 for commands and chap 5 for theory
+
 Language
 
-- Modules (see doc chap 2.5 for commands and chap 4 for theory)
 - Inductive definitions now accept ">" in constructor types to declare
   the corresponding constructor as a coercion.
 - Idem for assumptions declarations and constants when the type is mentionned.
@@ -64,6 +67,7 @@ ML tactic and vernacular commands
   COMMAND EXTEND.
 - "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..."
 - "Proof with T" (* no documentation *)
+-  SearchAbout id - prints all theorems which contain id in their type
 
 Tactic definitions
 
@@ -87,6 +91,9 @@ Tactics
   it can also recognize 'False' in the hypothesis and use it to solve the
   goal.
 - Coercions now handled in "with" bindings
+- "Subst x" replaces all ocurrences of x by t in the goal and hypotheses 
+   when an hypothesis x=t or x:=t or t=x exists
+- LinearIntuition (* no documentation *)
 
 Miscellaneous
 
-- 
cgit v1.2.3