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

[helm.git] / helm / matita / library / nat / gcd.ma

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.