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

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

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 *)