Nouveau lexeme METAIDENT pour les $id

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

1 files changed, 17 insertions, 11 deletions

diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 8951e94a8..7a09453af 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -7,11 +7,14 @@ open Pcoq
 open Prim
 
 GEXTEND Gram
-  GLOBAL: var ident number string path ast astpat astact entry_type;
+  GLOBAL: var ident metaident number string path ast astpat astact entry_type;
 
   var:
     [ [ s = IDENT -> Nvar(loc,s) ] ]
   ;
+  metaident:
+    [ [ s = METAIDENT -> Nvar(loc,s) ] ]
+  ;
   ident:
     [ [ s = IDENT -> Id(loc,s) ] ]
   ;
@@ -21,27 +24,30 @@ GEXTEND Gram
   string:
     [ [ s = STRING -> Str(loc,s) ] ]
   ;
-  path:
-    [ [ (l,pk) = qualid -> Path(loc,l,pk) ] ]
+  astpath:
+    [ [ (l,pk) = astqualid -> Path(loc,l,pk) ] ]
   ;
-  qualid:
+  astqualid:
     [ [ "#"; l = LIST1 IDENT SEP "#"; "."; pk = IDENT -> (l, pk) ] ]
   ;
-
+  astident:
+    [ [ s = IDENT -> s 
+      | s = METAIDENT -> s ] ]
+  ;
   (* ast *)
   ast:
-    [ [ id = IDENT -> Nvar(loc,id)
+    [ [ id = astident -> Nvar(loc,id)
       | s = INT -> Num(loc, int_of_string s)
       | s = STRING -> Str(loc,s)
-      | p = path -> p
+      | p = astpath -> p
       | "{"; s = IDENT; "}" -> Id(loc,s)
-      | "("; nname = IDENT; l = LIST0 ast; ")" -> Node(loc,nname,l)
-      | "["; ido = idoption; "]"; b = ast -> Slam(loc,ido,b)
+      | "("; nname = astident; l = LIST0 ast; ")" -> Node(loc,nname,l)
+      | "["; ido = astidoption; "]"; b = ast -> Slam(loc,ido,b)
       | "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
   ;
-  idoption:
+  astidoption:
     [ [ "<>" -> None
-      | id = IDENT -> Some id ] ]
+      | id = astident -> Some id ] ]
   ;
 
   (* meta-syntax entries *)