Ajout ne_string

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

3 files changed, 15 insertions, 1 deletions

diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index d41055fb6..63198f874 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -84,10 +84,12 @@ open Q
 
 if not !Options.v7 then
 GEXTEND Gram
-  GLOBAL: ast bigint qualid reference;
+  GLOBAL: (*ast*) bigint qualid reference ne_string;
+(*
   metaident:
     [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
   ;
+*)
   field:
     [ [ s = FIELD -> local_id_of_string s ] ]
   ;
@@ -96,12 +98,14 @@ GEXTEND Gram
       | id = field -> ([],id)
       ] ]
   ;
+(*
   astpath:
     [ [ id = base_ident; (l,a) = fields ->
           Path(loc, local_make_path (local_append l id) a)
       | id = base_ident -> Nvar(loc, id)
       ] ]
   ;
+*)
   basequalid:
     [ [ id = base_ident; (l,id')=fields ->
           local_make_qualid (local_append l id) id'
@@ -117,6 +121,12 @@ GEXTEND Gram
   qualid:
     [ [ qid = basequalid -> loc, qid ] ]
   ;
+  ne_string:
+    [ [ s = STRING -> 
+        if s="" then Util.user_err_loc(loc,"",Pp.str"Empty string"); s
+    ] ]
+  ;
+(*
   ast:
     [ [ id = metaident -> id
       | p = astpath -> p
@@ -135,6 +145,7 @@ GEXTEND Gram
       | "["; a = ast; "]"; b = ast -> local_make_binding loc a b
       | "'"; a = ast -> Node(loc,"$QUOTE",[a]) ] ]
   ;
+*)
   bigint: (* Negative numbers are dealt with specially *)
     [ [ i = INT -> Bignat.POS (Bignat.of_string i) ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 280c501a9..b9ec4cfc2 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -322,6 +322,8 @@ module Prim =
     let qualid = Gram.Entry.create "Prim.qualid"
     let dirpath = Gram.Entry.create "Prim.dirpath"
 
+    let ne_string = Gram.Entry.create "Prim.ne_string"
+
     (* For old ast printer *)
     let astpat = Gram.Entry.create "Prim.astpat"
     let ast = Gram.Entry.create "Prim.ast"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1bd6d4e7c..0541d1cf7 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -119,6 +119,7 @@ module Prim :
     val qualid : qualid located Gram.Entry.e
     val reference : reference Gram.Entry.e
     val dirpath : dir_path Gram.Entry.e
+    val ne_string : string Gram.Entry.e
     val astpat: typed_ast Gram.Entry.e
     val ast : Coqast.t Gram.Entry.e
     val astlist : Coqast.t list Gram.Entry.e