Essai d'une autre syntaxe pour la dlimitation des scopes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3333 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 9 insertions, 13 deletions

diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 7e1cf5da7a..647dc0a257 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -26,13 +26,11 @@ GEXTEND Gram
     [ [ r = Prim.reference -> CPatAtom (loc,Some r)
       | IDENT "_" -> CPatAtom (loc,None)
       (* Hack to parse syntax "(n)" as a natural number *)
-      | "("; G_constr.test_int_rparen; n = INT; ")" ->
-	  let n = CPatNumeral (loc,Bignat.POS (Bignat.of_string n)) in
-          CPatDelimiters (loc,"N",n)
+      | "("; G_constr.test_int_rparen; n = bigint; ")" ->
+          CPatDelimiters (loc,"N",CPatNumeral (loc,n))
       | "("; p = compound_pattern; ")" -> p
-      | n = INT -> CPatNumeral (loc,Bignat.POS (Bignat.of_string n))
-      | "-"; n = INT -> CPatNumeral (loc,Bignat.NEG (Bignat.of_string n))
-      | "`"; G_constr.test_ident_colon; key = string; ":"; c = pattern; "`" -> 
+      | n = bigint -> CPatNumeral (loc,n)
+      | "'"; G_constr.test_ident_colon; key = IDENT; ":"; c = pattern; "'" -> 
           CPatDelimiters (loc,key,c)
     ] ]
   ;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index c298b0e3ff..01b770288a 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -68,7 +68,7 @@ let test_int_bang =
 (* Hack to parse "`id:...`" at level 0 without conflicting with
    "`...`" from ZArith *)
 let test_ident_colon =
-  Gram.Entry.of_parser "test_int_bang"
+  Gram.Entry.of_parser "test_ident_colon"
     (fun strm ->
       match Stream.npeek 1 strm with
         | [("IDENT", _)] ->
@@ -146,9 +146,8 @@ GEXTEND Gram
       | "?"; n = Prim.natural -> CMeta (loc, n)
       | bll = binders; c = constr LEVEL "top" -> abstract_constr loc c bll
       (* Hack to parse syntax "(n)" as a natural number *)
-      | "("; test_int_rparen; n = INT; ")" ->
-	  let n = CNumeral (loc,Bignat.POS (Bignat.of_string n)) in
-          CDelimiters (loc,"N",n)
+      | "("; test_int_rparen; n = bigint; ")" ->
+          CDelimiters (loc,"N",CNumeral (loc,n))
       | "("; lc1 = lconstr; ":"; c = constr; (bl,body) = product_tail ->
           let id = coerce_to_name lc1 in
 	  CProdN (loc, ([id], c)::bl, body)
@@ -176,10 +175,9 @@ GEXTEND Gram
 	  CCoFix (loc, id, fbinders)
       | s = sort -> CSort (loc, s)
       | v = global -> CRef v
-      | n = INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
-      | "-"; n = INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n))
+      | n = bigint -> CNumeral (loc,n)
       | "!"; f = global -> CAppExpl (loc,f,[])
-      | "`"; test_ident_colon; key = string; ":"; c = constr; "`" -> 
+      | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> 
           CDelimiters (loc,key,c) ] ]
   ;
   lconstr: