X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Ftests%2Fmatch.ma;h=c75d4fda865ecc527962c94123506bbb2a7638eb;hb=31afc64440b7da53bb79e6f1524d47bf0fb56aaf;hp=3dbb580d5e105329ee325e043f17062be5e952f1;hpb=349a0e23813a7f33853e1f8fe48230276ac22934;p=helm.git

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index 3dbb580d5..c75d4fda8 100644
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -164,7 +164,7 @@ let rec minus n m \def
  match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow 
-	[\lambda n:nat.nat] match m with
+	match m with
 	[O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]].
 
@@ -280,7 +280,7 @@ let rec leb n m \def
     match n with 
     [ O \Rightarrow true
     | (S p) \Rightarrow
-	[\lambda n:nat.bool] match m with 
+	match m with 
         [ O \Rightarrow false
 	| (S q) \Rightarrow leb p q]].