diff options
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | dev/doc/perf-analysis | 8 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 6 |
3 files changed, 10 insertions, 6 deletions
@@ -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 = |