X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=ae4c0b3ef469f76a5471f2137fc3eb1fe9d68128;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=587c22e4a07b8b9a39fea3225069c4a73454e01f;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 587c22e4a..ae4c0b3ef 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -211,8 +211,8 @@ let extract_term_production pattern =
           match magic with
           | Ast.List0 (_, None) -> Gramext.Slist0 s
           | Ast.List1 (_, None) -> Gramext.Slist1 s
-          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l, false)
-          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l, false)
+          | Ast.List0 (_, Some l) -> Gramext.Slist0sep (s, gram_of_literal l,false)
+          | Ast.List1 (_, Some l) -> Gramext.Slist1sep (s, gram_of_literal l,false)
           | _ -> assert false
         in
         [ Env (List.map Env.list_declaration p_names),
@@ -246,14 +246,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 res = 
-            try Pervasives.compare s1 s2 
-            with Invalid_argument _ -> 0 
-          in
-           if res = 0 then aux (tl1, tl2) else res 
+        else Pervasives.compare x y 
   in
     aux (x,y)