]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationParser.ml
Release 0.5.9.
[helm.git] / helm / software / components / content_pres / cicNotationParser.ml
index 587c22e4a07b8b9a39fea3225069c4a73454e01f..ae4c0b3ef469f76a5471f2137fc3eb1fe9d68128 100644 (file)
@@ -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)