From fba8e67f0cec873727ad4612cfc8adf674582dba Mon Sep 17 00:00:00 2001
From: mohring
Date: Fri, 17 Jan 2003 15:11:24 +0000
Subject: *** empty log message ***

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

diff --git a/CHANGES b/CHANGES
index e2ff2025c6..c0ec7c8df0 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,8 +1,6 @@
-Changes from V7.3.1 to ????
+Changes from V7.3.1 to V7.4
 -------------------------
 
-TODO: unification 2eme ordre avec NewDestruct
-
 Grammar extension
 
 - In old syntax, the only predefined non-terminal entries are ident,
@@ -39,6 +37,7 @@ Library
 
 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.
@@ -65,6 +64,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 *)
+
 Tactic definitions
 
 - static globalisation of identifiers and global references (source of
-- 
cgit v1.2.3