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

diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma
index c952d0a92..3dbb580d5 100644
--- a/helm/matita/tests/match.ma
+++ b/helm/matita/tests/match.ma
@@ -1,3 +1,18 @@
+(**************************************************************************)
+(*       ___	                                                          *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *) 
+(*      ||I||       Developers:                                           *) 
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)   
+(*                                                                        *)
+(**************************************************************************)
+
+
 inductive True: Prop \def
 I : True.
 
@@ -97,7 +112,7 @@ intros.elim n.apply O_S.apply not_eq_S.assumption.
 qed.
 
 
-let rec plus n m : nat \def 
+let rec plus n m \def 
  match n with 
  [ O \Rightarrow m
  | (S p) \Rightarrow S (plus p m) ].
@@ -120,7 +135,7 @@ theorem assoc_plus:
 intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption.
 qed.
 
-let rec times n m : nat \def 
+let rec times n m \def 
  match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow (plus m (times p m)) ].
@@ -145,8 +160,8 @@ intros.elim n.simplify.apply times_n_O.
 simplify.elim (sym_eq ? ? ? H).apply times_n_Sm.
 qed.
 
-let rec minus n m : nat \def 
- [\lambda n:nat.nat] match n with 
+let rec minus n m \def 
+ match n with 
  [ O \Rightarrow O
  | (S p) \Rightarrow 
 	[\lambda n:nat.nat] match m with
@@ -261,8 +276,8 @@ apply le_S_n.assumption.
 apply le_S_n.assumption.
 qed.
 
-let rec leb n m : bool \def 
-   [\lambda n:nat.bool] match n with 
+let rec leb n m \def 
+    match n with 
     [ O \Rightarrow true
     | (S p) \Rightarrow
 	[\lambda n:nat.bool] match m with