Few misc. updates.

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

3 files changed, 10 insertions, 6 deletions

diff --git a/CHANGES b/CHANGES
index fac3d90343..9fdbc6ab0b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -126,6 +126,8 @@ Library
 - Lemmas in library Relations and Reals have been homogenized a bit.
 - The implicit argument of Logic.eq is now maximally inserted, allowing
   to simply write "eq" instead of "@eq _" in morphism signatures.
+- Light revision and extension of the List library (possible source
+  of incompatibilities solvable by qualifying names accordingly).
 - Revision of the Sorting library:
   - new mergesort of worst-case complexity O(n*ln(n)) made available in 
     Mergesort.v;
diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index 8e48154470..d23bf835b4 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,6 +1,14 @@
 Performance analysis (trunk repository)
 ---------------------------------------
 
+Dec 1, 2009 - Dec 19, 2009: Temporary addition of [forall x, P x] hints to
+  exact (generally not significative but, e.g., +25% on Subst, +8% on
+  ZFC, +5% on AreaMethod)
+
+Oct 19, 2009: Change in modules (CoLoR +35%)
+
+Aug 9, 2009: new files added in AreaMethod 
+
 May 21, 2008: New version of CoRN
   (needs +84% more time to compile)
 
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index dc57e4aadc..a2dd7d777d 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -52,12 +52,6 @@ open Subtac_obligations
 let evar_nf isevars c =
   Evarutil.nf_isevar !isevars c
 
-let get_undefined_evars evd =
-  Evd.fold (fun ev evi evd' ->
-    if evi.evar_body = Evar_empty then
-      Evd.add evd' ev (nf_evar_info evd evi)
-    else evd') evd Evd.empty
-
 let interp_gen kind isevars env
                ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[]))
                c =