From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 19 Oct 2010 13:25:32 +0000 (+0000)
Subject: camlp5 probably changed some internal data structures and now they cannot be compared... 
X-Git-Tag: make_still_working~2772
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b7e730726f5c5ba9b53b80d3881bcacd38a11a67;p=helm.git

camlp5 probably changed some internal data structures and now they cannot be compared with pervasives.comapre, thus we avoid it. Was breaking the natural deduction stuff
---

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 829e78b6d..95b688c54 100644
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -246,9 +246,14 @@ let compare_rule_id x y =
     | [],[] -> 0
     | [],_ -> ~-1
     | _,[] -> 1
-    | ((s1::tl1) as x),((s2::tl2) as y) ->
+    | ((s1::tl1) ),((s2::tl2) ) ->
         if Gramext.eq_symbol s1 s2 then aux (tl1,tl2)
-        else Pervasives.compare x y 
+        else 
+          let res = 
+            try Pervasives.compare s1 s2 
+            with Invalid_argument _ -> 0 
+          in
+           if res = 0 then aux (tl1, tl2) else res 
   in
     aux (x,y)