'Grammar tactic' devient 'Tactic Notation'

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

1 files changed, 13 insertions, 7 deletions

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 34bdbbb8c..1522d6fa6 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -682,10 +682,16 @@ GEXTEND Gram
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
            VernacNotation (local,c,Some(s,modl),None,sc)
 
+     | IDENT "Tactic"; IDENT "Notation"; s = STRING; 
+	 pil = LIST0 production_item; ":="; t = Tactic.tactic -> 
+	   VernacTacticGrammar ["",(s,pil),t]
+
+(*
      | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
-        OPT [ ":"; IDENT "tactic" ]; ":=";
+        (* OPT [ ":"; IDENT "tactic" ]; *) ":=";
         OPT "|"; tl = LIST0 grammar_tactic_rule SEP "|" -> 
 	  VernacTacticGrammar tl
+*)
 
      | IDENT "Grammar"; u = univ;
          tl = LIST1 grammar_entry SEP "with" -> 
@@ -751,10 +757,12 @@ GEXTEND Gram
      | IDENT "NONA" -> Some Gramext.NonA
      | -> None ]]
   ;
+(*
   grammar_tactic_rule:
-    [[ name = rule_name; "["; s = STRING; pil = LIST0 production_item; "]";
-       "->"; "["; t = Tactic.tactic; "]"  -> (name, (s,pil), t) ]]
+    [[ (* name = rule_name; *) "["; s = STRING; pil = LIST0 production_item; "]";
+       "->"; "["; t = Tactic.tactic; "]"  -> let name="" in (name,(s,pil),t) ]]
   ;
+*)
   grammar_rule:
     [[ name = rule_name; "["; pil = LIST0 production_item; "]"; "->";
        a = action -> (name, pil, a) ]]
@@ -764,10 +772,8 @@ GEXTEND Gram
   ;
   production_item:
     [[ s = STRING -> VTerm s
-     | nt = non_terminal; po = OPT [ "("; p = METAIDENT; ")" -> p ] ->
-         match po with
-           | Some p -> VNonTerm (loc,nt,Some (Names.id_of_string p))
-           | _ -> VNonTerm (loc,nt,None) ]]
+     | nt = non_terminal; po = OPT [ "("; p = ident; ")" -> p ] ->
+	 VNonTerm (loc,nt,po) ]]
   ;
   non_terminal:
     [[ u = IDENT; ":"; nt = IDENT ->