X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=859697cd632ecf08c3b2f3d6debd5155f5e3e4eb;hb=6e785555b301cc1abe1671de3bd970aebebce71a;hp=f58bd21b59b460295d196e3a095f626ac8298e48;hpb=3e1e59644a24ed855a7f21bf9eab76f96577fd17;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index f58bd21b5..859697cd6 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -214,6 +214,17 @@ let extract_term_production pattern =
 
 type rule_id = Grammar.token Gramext.g_symbol list
 
+let compare_rule_id x y =
+  let rec aux = function
+    | [],[] -> 0
+    | [],_ -> ~-1
+    | _,[] -> 1
+    | ((s1::tl1) as x),((s2::tl2) as y) ->
+        if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
+        else Pervasives.compare x y 
+  in
+    aux (x,y)
+
   (* mapping: rule_id -> owned keywords. (rule_id, string list) Hashtbl.t *)
 let owned_keywords = Hashtbl.create 23