X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=95b688c548b0f4565dcecddff4c777e26477c546;hb=12023ae1e3d075130b31d2d8559c85847ef06dee;hp=af9edd9be226bb54bd30f714df9144b70ebd6c1c;hpb=2d3d1750a0012ebc45f97d0000c01141623fc634;p=helm.git

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index af9edd9be..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)
 
@@ -581,9 +586,9 @@ EXTEND
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
-    | "Type"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NType n
+    | "Type"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NType n
     | "Type" -> `Type (CicUniv.fresh ()) 
-    | "CProp"; SYMBOL "["; n = NUMBER; SYMBOL "]" -> `NCProp n
+    | "CProp"; SYMBOL "["; n = [ NUMBER| IDENT ]; SYMBOL "]" -> `NCProp n
     | "CProp" -> `CProp (CicUniv.fresh ())
     ]
   ];
@@ -714,8 +719,8 @@ EXTEND
   [
     [ "let"; 
      var = 
-      [ LPAREN; id = IDENT; SYMBOL ":"; typ = term; RPAREN ->
-	  Ast.Ident(id,None), Some typ
+      [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
+	  id, Some typ
       | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
 	  Ast.Ident(id,None), ty ];
       SYMBOL <:unicode<def>> (* ≝ *);
@@ -816,6 +821,8 @@ let exc_located_wrapper f =
   with
   | Stdpp.Exc_located (floc, Stream.Error msg) ->
       raise (HExtlib.Localized (floc, Parse_error msg))
+  | Stdpp.Exc_located (floc, HExtlib.Localized (_,exn)) ->
+      raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))
   | Stdpp.Exc_located (floc, exn) ->
       raise (HExtlib.Localized (floc, (Parse_error (Printexc.to_string exn))))