From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 5 Oct 2005 09:04:43 +0000 (+0000)
Subject: separated "]]" to avoid clash with (temporary) continuationals ligatures
X-Git-Tag: V_0_7_2_3~249
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5433a131a7ff29529747e58c68dbf258d696e55b;p=helm.git

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 0456ca0b3..c1db18b18 100644
--- 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 eb1053feb..90de2013a 100644
--- 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 d0e2b98f0..1992121b6 100644
--- 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 *)