Syntactic change:

 [ ... ] match t in t with ==> match t in t return ... with

diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma
index 2848c08c5753086d5ffb5e9073c1b2687ee95bae..4cbea3529a7ec983b39f814f1243f1a5f92568ab 100644 (file)
--- 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 7e67c056ca9a9f74bd503fe752d904781e437200..40157d849f9baf53e9f871f07ef5432adba152c9 100644 (file)
--- 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 94e4ee367a605dd48b41bab97d28986044368b45..0abed5ad354319674d89e049ca833f804cdaaeec 100644 (file)
--- 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 9f917d0b3ca7d670ae08f73edd1c681fbef67edd..3241d239e6f225f2b8273203d77dd81305ba8c12 100644 (file)
--- 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>