From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 9 Jun 2005 16:08:57 +0000 (+0000)
Subject: No more explicit types for the branches of the matches: all the bugs
X-Git-Tag: PRE_INDEX_1~8
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1e341b177cc490278c4b9561f7ba3eeb41a1ab0f;p=helm.git

No more explicit types for the branches of the matches: all the bugs
preventing automatic type inference have been fixed.
---

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]].