From 0d25cb99daa91fdc3b2ceedc87c6c1480e8577b6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 17 May 2005 13:23:34 +0000
Subject: Affinements suite à extension Tactic Notation aux tacticielles

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7030 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/egrammar.ml      | 8 ++++++--
 parsing/g_basevernac.ml4 | 2 +-
 parsing/g_vernacnew.ml4  | 2 +-
 parsing/tacextend.ml4    | 8 ++++++--
 4 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index aa2558ddab..1acf41ec6c 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -438,16 +438,20 @@ let get_tactic_entry n =
 
 open Tacexpr
 
+let head_is_ident = function (_,VTerm _::_,_) -> true | _ -> false
+
 let add_tactic_entries (lev,gl) =
   let univ = get_univ "tactic" in
   let entry, pos = get_tactic_entry lev in
   let rules = 
-    if lev = 0 then
+    if lev = 0 then begin
+      if not (List.for_all head_is_ident gl) then
+	error "Notations for simple tactics must start with an identifier";
       let make_act s tac loc l = 
 	(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
       let f (s,l,tac) =
 	make_rule univ (make_act s tac) (make_vprod_item lev "tactic") l in
-      List.map f gl
+      List.map f gl end
     else
       let make_act s tac loc l = 
 	(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 097f38f01d..aab672153d 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -424,7 +424,7 @@ GEXTEND Gram
      | -> None ]]
   ;
   grammar_tactic_rule:
-    [[ name = rule_name; "["; pil = LIST0 production_item; "]";
+    [[ name = rule_name; "["; pil = LIST1 production_item; "]";
        "->"; "["; t = Tactic.tactic; "]"  -> (name, pil, t) ]]
   ;
   grammar_rule:
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index c21feb09e8..f839e8f212 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -694,7 +694,7 @@ GEXTEND Gram
            VernacNotation (local,c,Some(s,modl),None,sc)
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; 
-	 pil = LIST0 production_item; ":="; t = Tactic.tactic
+	 pil = LIST1 production_item; ":="; t = Tactic.tactic
          -> VernacTacticGrammar (n,["",pil,t])
 
      | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; 
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 3a20aad1b5..21b96c8a7f 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -267,8 +267,12 @@ EXTEND
          declare_tactic_v7 loc s l ] ]
   ;
   tacrule:
-    [ [ "["; l = LIST0 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]"
-        -> (l,e)
+    [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]"
+        -> 
+	  if match List.hd l with TacNonTerm _ -> true | _ -> false then
+	    (* En attendant la syntaxe de tacticielles *)
+	    failwith "Tactic syntax must start with an identifier";
+	  (l,e)
     ] ]
   ;
   tacargs:
-- 
cgit v1.2.3