Mises à jour bugs, CHANGES, code mort

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

4 files changed, 3 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 506da926d..1c3fe7b4c 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 
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 072d664fc..ed9d779ad 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -231,7 +231,6 @@ let dependent_metas clenv mvs conclmetas =
     mvs conclmetas
 
 let clenv_dependent hyps_only clenv =
-  let mvs = collect_metas (clenv_value clenv) in
   let mvs = undefined_metas clenv.evd in
   let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
   let deps = dependent_metas clenv mvs ctyp_mvs in
diff --git a/test-suite/bugs/opened/shouldnotfail/1774.v b/test-suite/bugs/closed/shouldsucceed/1774.v
index 4c24b481b..4c24b481b 100644
--- a/test-suite/bugs/opened/shouldnotfail/1774.v
+++ b/test-suite/bugs/closed/shouldsucceed/1774.v
diff --git a/test-suite/bugs/opened/shouldnotfail/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v
index dab4120b9..dab4120b9 100644
--- a/test-suite/bugs/opened/shouldnotfail/1775.v
+++ b/test-suite/bugs/closed/shouldsucceed/1775.v