From cb586ea65a1ad38626b7481ff8b30007f488705d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Jun 2010 10:08:53 +0000
Subject: Backported r13080 (support for open terms in ltac matching) from
 trunk to v8.3. Also updated perf-analysis file (the part of the commit that
 delays typing of ltac instances seems to slightly improve a few
 contributions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13096 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/doc/perf-analysis | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'dev/doc')

diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index 805f0778d1..ac54fa6f73 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,9 +1,13 @@
 Performance analysis (trunk repository)
 ---------------------------------------
 
-Jun 4, 2010: improvement in type classes inference by removing
+Jun 7, 2010: delayed re-typing of Ltac instances in matching
+  (-1% on HighSchoolGeometry, -2% on JordanCurveTheorem)
+
+Jun 4, 2010: improvement in eauto and type classes inference by removing
   systematic preparation of debugging pretty-printing streams (std_ppcmds)
-  (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk)
+  (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk;
+   -6% in HighSchoolGeometry)
 
 Apr 19, 2010: small improvement obtained by reducing evar instantiation 
   from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert,
-- 
cgit v1.2.3