Mises à jour bugs, CHANGES, code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10801 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 3 deletions

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