From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 21 Jun 2011 20:35:04 +0000 (+0000)
Subject: missing ; to delimit syntax :(
X-Git-Tag: make_still_working~2420
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=052c5c2ca4c5257716ada059fbc723c975428a61;p=helm.git

missing ; to delimit syntax :(
---

diff --git a/matita/matita/lib/basics/list.ma b/matita/matita/lib/basics/list.ma
index e4bdcb8aa..8b0449987 100644
--- a/matita/matita/lib/basics/list.ma
+++ b/matita/matita/lib/basics/list.ma
@@ -211,9 +211,8 @@ lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
 #A #n elim n -n //
 #n #IHn #l elim l normalize //
 qed.
-(*
+
 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
 #A #n elim n -n /2/
-#n #IHn * normalize /2/
+#n #IHn *; normalize /2/
 qed.
-*)
\ No newline at end of file