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 3dbb580d5e105329ee325e043f17062be5e952f1..c75d4fda865ecc527962c94123506bbb2a7638eb 100644 (file)
--- 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]].