From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 4 Sep 2008 10:38:48 +0000 (+0000)
Subject: comparison function fixed
X-Git-Tag: make_still_working~4820
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=794fe0432b14ca29e5dfd2e217cef72e9b0ff61a;p=helm.git

comparison function fixed
---

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 5236193d0..859697cd6 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -219,11 +219,9 @@ let compare_rule_id x y =
     | [],[] -> 0
     | [],_ -> ~-1
     | _,[] -> 1
-    | s1::tl1, s2::tl2 ->
+    | ((s1::tl1) as x),((s2::tl2) as y) ->
         if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
-        else 
-          let d = List.length tl1 - List.length tl2 in
-          if d <> 0 then d else 1 (* bad and broken *)
+        else Pervasives.compare x y 
   in
     aux (x,y)