]> matita.cs.unibo.it Git - helm.git/commitdiff
comparison function fixed
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 Sep 2008 10:38:48 +0000 (10:38 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 Sep 2008 10:38:48 +0000 (10:38 +0000)
helm/software/components/content_pres/cicNotationParser.ml

index 5236193d054257091e2962ea626d20f90122777d..859697cd632ecf08c3b2f3d6debd5155f5e3e4eb 100644 (file)
@@ -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)