]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationParser.ml
snapshot
[helm.git] / helm / software / components / content_pres / cicNotationParser.ml
index f58bd21b59b460295d196e3a095f626ac8298e48..859697cd632ecf08c3b2f3d6debd5155f5e3e4eb 100644 (file)
@@ -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