Ajout option 'Local' à Infix et Notation

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

3 files changed, 34 insertions, 25 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 3d97537832..3db24bcd12 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -241,12 +241,12 @@ GEXTEND Gram
      | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP ";" ->
          VernacSyntax (u,el)
 
-     | IDENT "Uninterpreted"; IDENT "Notation"; s = STRING; 
+     | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (s,l)
+	 -> VernacSyntaxExtension (local,s,l)
 
-     | IDENT "Open"; exp = [IDENT "Local" -> false | -> true]; IDENT "Scope"; 
-	 sc = IDENT -> VernacOpenScope (exp,sc)
+     | IDENT "Open"; local = locality; IDENT "Scope"; 
+	 sc = IDENT -> VernacOpenScope (local,sc)
 
      | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -254,7 +254,7 @@ GEXTEND Gram
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
 
-     | IDENT "Infix"; a = entry_prec; n = OPT natural;
+     | IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural;
          op = STRING; 
          p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
@@ -277,12 +277,13 @@ GEXTEND Gram
            let (a8,n8,_) =
              Metasyntax.interp_infix_modifiers a nv8 mv8 in
            let v8 = Some(a8,n8,op8) in
-           VernacInfix (ai,ni,op,p,b,v8,sc)
-     | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = global;
-	 sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc)
-     | IDENT "Notation"; s = IDENT; ":="; c = constr ->
-	 VernacNotation ("'"^s^"'",c,[],None,None)
-     | IDENT "Notation"; s = STRING; ":="; c = constr;
+           VernacInfix (local,ai,ni,op,p,b,v8,sc)
+     | IDENT "Distfix"; local = locality; a = entry_prec; n = natural; 
+	   s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
+	     VernacDistfix (local,a,n,s,p,sc)
+     | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr ->
+	 VernacNotation (local,"'"^s^"'",c,[],None,None)
+     | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ];
          (s8,mv8) =
@@ -295,12 +296,15 @@ GEXTEND Gram
                let mv8 = match mv8 with
                    Some mv8 -> mv8
                  | _ -> List.map map_modl modl in
-               VernacNotation (s,c,modl,Some(s8,mv8),sc)
+               VernacNotation (local,s,c,modl,Some(s8,mv8),sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
   ] ]
   ;
+  locality:
+    [ [ IDENT "Local" -> true | -> false ] ]
+  ;
   syntax_modifier:
     [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> 
         SetItemLevel ([x],n)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cb02b082e4..2d1fcdd306 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -419,7 +419,7 @@ GEXTEND Gram
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
 		 CApp (loc,c,l)
 	     | None -> c in
-	   VernacNotation ("'"^id^"'",c,[],None,None)
+	   VernacNotation (false,"'"^id^"'",c,[],None,None)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 0ad8caaaa0..0e9e8dabbd 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -411,6 +411,7 @@ GEXTEND Gram
 	  VernacCoercion (Global, qid, s, t)
 
       (* Implicit *)
+(* Obsolete
       | IDENT "Syntactic"; IDENT "Definition"; id = IDENT; ":="; c = lconstr;
          n = OPT [ "|"; n = natural -> n ] ->
 	   let c = match n with
@@ -418,7 +419,8 @@ GEXTEND Gram
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
 		 CApp (loc,c,l)
 	     | None -> c in
-	   VernacNotation ("'"^id^"'",c,[],None,None)
+	   VernacNotation (false,"'"^id^"'",c,[],None,None)
+*)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
@@ -648,8 +650,8 @@ GEXTEND Gram
   GLOBAL: syntax;
 
   syntax:
-   [ [ IDENT "Open"; exp = [IDENT "Local" -> false | -> true]; IDENT "Scope"; 
-       sc = IDENT -> VernacOpenScope (exp,sc)
+   [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> 
+         VernacOpenScope (local,sc)
 
      | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -657,18 +659,18 @@ GEXTEND Gram
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
 
-     | IDENT "Infix"; a = entry_prec; n = OPT natural; op = STRING; 
-         p = global;
+     | IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural; 
+	 op = STRING; p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in
-         VernacInfix (a,n,op,p,b,None,sc)
-     | IDENT "Notation"; s = IDENT; ":="; c = constr ->
-	 VernacNotation ("'"^s^"'",c,[],None,None)
-     | IDENT "Notation"; s = STRING; ":="; c = constr;
+         VernacInfix (local,a,n,op,p,b,None,sc)
+     | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr ->
+	 VernacNotation (local,"'"^s^"'",c,[],None,None)
+     | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (s,c,modl,None,sc)
+           VernacNotation (local,s,c,modl,None,sc)
 
      | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
         OPT [ ":"; IDENT "tactic" ]; ":=";
@@ -682,14 +684,17 @@ GEXTEND Gram
      | IDENT "Syntax"; u = univ; el = LIST1 syntax_entry SEP "," ->
          VernacSyntax (u,el)
 
-     | IDENT "Uninterpreted"; IDENT "Notation"; s = STRING; 
+     | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (s,l)
+	 -> VernacSyntaxExtension (local,s,l)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
   ] ]
   ;
+  locality:
+    [ [ IDENT "Local" -> true | -> false ] ]
+  ;
   univ:
   [ [ univ = IDENT ->
         set_default_action_parser (parser_type_from_name univ); univ ] ]