1. syntax of match changed

2. syntax of the bindings of "let rec" made lighter

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index 21bad46a9f8ab8d2c0e5d2c236860c9805c3eaec..2382ba7b71f6a22e1f740e57c6e2d9b5cbc03750 100644 (file)
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -98,8 +98,8 @@ qed.
 
 
 definition plus : nat \to nat \to nat \def
-let rec plus (n,m:nat) \def 
- match n:nat with 
+let rec plus (n,m) \def 
+ match n with 
  [ O \Rightarrow m
  | (S p) \Rightarrow S (plus p m) ]
 in
@@ -124,8 +124,8 @@ intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 qed.
 
 definition times : nat \to nat \to nat \def
-let rec times (n,m:nat) \def 
- match n:nat with 
+let rec times (n,m) \def 
+ match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow (plus m (times p m)) ]
 in
@@ -152,11 +152,11 @@ simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 qed.
 
 definition minus : nat \to nat \to nat \def
-let rec minus (n,m:nat) \def 
- [\lambda n:nat.nat] match n:nat with 
+let rec minus (n,m) \def 
+ [\lambda n:nat.nat] match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow 
-       [\lambda n:nat.nat] match m:nat with
+       [\lambda n:nat.nat] match m with
        [O \Rightarrow (S p)
         | (S q) \Rightarrow minus p q ]]
 in
@@ -271,11 +271,11 @@ apply le_S_n.assumption.
 qed.
 
 definition leb : nat \to nat \to bool \def
-let rec leb (n,m:nat) \def 
-   [\lambda n:nat.bool] match n:nat with 
+let rec leb (n,m) \def 
+   [\lambda n:nat.bool] match n with 
     [ O \Rightarrow true
     | (S p) \Rightarrow
-       [\lambda n:nat.bool] match m:nat with 
+       [\lambda n:nat.bool] match m with 
         [ O \Rightarrow false
        | (S q) \Rightarrow leb p q]]
 in leb.
@@ -300,6 +300,6 @@ let square \def (times eightyone eightyone) in
 intro.
 intro.
 intro.intro.
-normalize goal at (? ? % ?).
+STOP normalize goal at (? ? % ?).