From f907cc977bb80e3654174de03aeaed2cb4aa4a7e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 15 Apr 2008 16:35:54 +0000
Subject: Mises à jour bugs, CHANGES, code mort

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 506da926d0..1c3fe7b4c1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -21,16 +21,16 @@ Commands
 
 - Added option Global to "Arguments Scope" for section surviving. (DOC TODO)
 - Added option "Unset Elimination Schemes" to deactivate the automatic
-  generation of elimination schemes. (DOC TODO)
+  generation of elimination schemes.
 - Modification of the Scheme command so you can ask for the name to be
-  automatically computed (e.g. Scheme Induction for nat Sort Set). (DOC TODO?)
+  automatically computed (e.g. Scheme Induction for nat Sort Set).
 - New command "Combined Scheme" to build combined mutual induction
   principles from existing mutual induction principles. 
 - New command "Scheme Equality" to build a decidable (boolean) equality 
   for simple inductive datatypes and a decision property over this equality
   (e.g.  Scheme Equality for nat).
 - Added option "Set Equality Scheme" to make automatic the declaration 
-  of the boolean equality when possible. (DOC TODO?)
+  of the boolean equality when possible.
 - Source of universe inconsistencies now printed when option 
   "Set Printing Universes" is activated,
 - Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the 
-- 
cgit v1.2.3