From 8530992b72238902faae5e8bff74550fd8d7264a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 13:52:50 +0000
Subject: [PATCH] Syntactic change:  [ ... ] match t in t with ==> match t in t
 return ... with

---
 helm/matita/library/logic/connectives.ma | 3 +--
 helm/matita/library/logic/equality.ma    | 3 +--
 helm/matita/library/nat/minimization.ma  | 4 ++--
 helm/matita/matita.lang                  | 1 +
 4 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 2848c08c5..4cbea3529 100644
--- a/helm/matita/library/logic/connectives.ma
+++ b/helm/matita/library/logic/connectives.ma
@@ -65,8 +65,7 @@ theorem Or_ind':
     \forall p:A \lor B. P p.
  intros.
  apply
-  ([\lambda p.P p]
-   match p with
+  (match p return \lambda p.P p with
     [(or_introl p) \Rightarrow H p
     |(or_intror q) \Rightarrow H1 q]).
 qed.
diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma
index 7e67c056c..40157d849 100644
--- a/helm/matita/library/logic/equality.ma
+++ b/helm/matita/library/logic/equality.ma
@@ -32,8 +32,7 @@ theorem eq_ind':
   P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
  intros.
  exact
-  ([\lambda y. \lambda p.P y p]
-   match p with
+  (match p return \lambda y. \lambda p.P y p with
     [refl_eq \Rightarrow H]).
 qed.
  
diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index 94e4ee367..0abed5ad3 100644
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -85,7 +85,7 @@ apply (le_n_O_elim a H2).intro.simplify.rewrite > H4.
 simplify.assumption.
 simplify.
 apply (bool_ind (\lambda b:bool.
-(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (S n1) = b) \to (f (match b in bool with
 [ true \Rightarrow (S n1)
 | false  \Rightarrow (max n1 f)])) = true)).
 simplify.intro.assumption.
@@ -160,7 +160,7 @@ rewrite > (min_aux_O_f f).rewrite < Hcut.assumption.
 apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption.
 simplify.
 apply (bool_ind (\lambda b:bool.
-(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (m-(S n)) = b) \to (f (match b in bool with
 [ true \Rightarrow m-(S n)
 | false  \Rightarrow (min_aux n m f)])) = true)).
 simplify.intro.assumption.
diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 9f917d0b3..3241d239e 100644
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -44,6 +44,7 @@
     <keyword>qed</keyword>
     <keyword>rec</keyword>
     <keyword>record</keyword>
+    <keyword>return</keyword>
     <keyword>to</keyword>
     <keyword>using</keyword>
     <keyword>with</keyword>
-- 
2.39.2