performance data for basic_1 on dev.helm

diff --git a/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt b/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt
index a4972af9c5f4e8b2ffabebe811422c6bc415bb19..6c46086eaafeb7c970292022fabd9452d38c4a79 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt
+++ b/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt
@@ -1,9 +1,17 @@
-full validation of lambdadelta_1 on "monica"
-
-date: ven  6 mar 2015, 20.31.46, CET
+full validation of lambdadelta_1
 
 command: time ../../matitac.opt basic_1
 
-real    4m39.904s
-user    3m58.580s
-sys     0m11.473s
+- machine: "monica"
+  date   : ven  6 mar 2015, 20.31.46, CET
+
+  real    4m39.904s
+  user    3m58.580s
+  sys     0m11.473s
+
+- machine: "dev.helm"
+  date   : Sat Mar  7 16:41:46 CET 2015
+
+  real    30m36.357s
+  user    6m35.749s
+  sys     0m31.518s

diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
index 8738e723477753937d43b49254e1449b438b7f0d..518bb5ff064f169a3128a6d89ad55521c865d2c8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
+++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma
@@ -90,5 +90,5 @@ let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to Prop)) (f:
 (\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall 
 (y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a 
 \def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y: 
-A).(\lambda (r: (R y x)).((Acc_ind A R P f) y (a1 y r)))))].
+A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))].