separated "]]" to avoid clash with (temporary) continuationals ligatures

diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma
index 0456ca0b31533f5aed0ccc9fd7561d67b2b3b2bd..c1db18b18d949b5573cb93829bb8f3c721cad605 100644 (file)
--- a/helm/matita/library/Z/plus.ma
+++ b/helm/matita/library/Z/plus.ma
@@ -29,7 +29,7 @@ definition Zplus :Z \to Z \to Z \def
               match nat_compare m n with
                 [ LT \Rightarrow (neg (pred (n-m)))
                 | EQ \Rightarrow OZ
-                | GT \Rightarrow (pos (pred (m-n)))]]
+                | GT \Rightarrow (pos (pred (m-n)))] ]
     | (neg m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
@@ -38,7 +38,7 @@ definition Zplus :Z \to Z \to Z \def
                 [ LT \Rightarrow (pos (pred (n-m)))
                 | EQ \Rightarrow OZ
                 | GT \Rightarrow (neg (pred (m-n)))]     
-         | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]].
+         | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y).

diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma
index eb1053feb78cb5e88a70a9154ff9af271f15e08b..90de2013a5e9f9ba02f681e2cfe7d4761179897b 100644 (file)
--- a/helm/matita/library/nat/gcd.ma
+++ b/helm/matita/library/nat/gcd.ma
@@ -115,7 +115,7 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m
 \land
 match leb n m with
   [ true \Rightarrow 
@@ -125,7 +125,7 @@ match leb n m with
   | false \Rightarrow 
     match m with 
     [ O \Rightarrow n
-    | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n. 
+    | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n. 
 apply leb_elim n m.
 apply nat_case1 n.
 simplify.intros.split.

diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma
index d0e2b98f0a7ad48427a2ba746ef35d85ea8d4e4e..1992121b61e60de97ca29590f749117b408f4135 100644 (file)
--- a/helm/matita/library/nat/ord.ma
+++ b/helm/matita/library/nat/ord.ma
@@ -28,7 +28,7 @@ let rec p_ord_aux p n m \def
       [ O \Rightarrow pair nat nat O n
       | (S p) \Rightarrow 
        match (p_ord_aux p (n / m) m) with
-       [ (pair q r) \Rightarrow pair nat nat (S q) r]]
+       [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
   | (S a) \Rightarrow pair nat nat O n].
   
 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)