Simplifification de vernac_expr li l'abandon du traducteur

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

3 files changed, 23 insertions, 34 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index e0d877b66..be8b1e8ad 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -21,16 +21,14 @@ open Nameops
 (* State of the grammar extensions *)
 
 type notation_grammar = 
-    int * Gramext.g_assoc option * notation * prod_item list * int list option
+    int * Gramext.g_assoc option * notation * prod_item list
 
 type all_grammar_command =
   | Notation of Notation.level * notation_grammar
   | Grammar of grammar_command
-  | TacticGrammar of 
-      int *
-      (string * grammar_production list *
-       (Names.dir_path * Tacexpr.glob_tactic_expr))
-      list
+  | TacticGrammar of
+      (string * int * grammar_production list * 
+        (Names.dir_path * Tacexpr.glob_tactic_expr))
 
 let (grammar_state : all_grammar_command list ref) = ref []
 
@@ -318,12 +316,8 @@ let extend_constr entry (n,assoc,pos,p4assoc,name) make_act (forpat,pt) =
   let act = make_act ntl in
   grammar_extend entry pos [(name, p4assoc, [symbs, act])]
 
-let extend_constr_notation (n,assoc,ntn,rule,permut) =
-  let mkact =
-    match permut with
-        None -> (fun loc env -> CNotation (loc,ntn,List.map snd env))
-      | Some p -> (fun loc env ->
-          CNotation (loc,ntn,List.map (fun i -> snd (List.nth env i)) p)) in
+let extend_constr_notation (n,assoc,ntn,rule) =
+  let mkact loc env = CNotation (loc,ntn,List.map snd env) in
   let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in
   let pos,p4assoc,name = find_position false keepassoc assoc level in
   extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name)
@@ -438,34 +432,31 @@ let get_tactic_entry n =
 
 open Tacexpr
 
-let head_is_ident = function (_,VTerm _::_,_) -> true | _ -> false
+let head_is_ident = function VTerm _::_ -> true | _ -> false
 
-let add_tactic_entries (lev,gl) =
+let add_tactic_entry (key,lev,prods,tac) =
   let univ = get_univ "tactic" in
   let entry, pos = get_tactic_entry lev in
   let rules = 
     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";
+      if not (head_is_ident prods) then
+	error "Notation for simple tactic 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 end
+      make_rule univ (make_act key tac) (make_vprod_item lev "tactic") prods
+    end
     else
       let make_act s tac loc l = 
 	(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_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 in
+      make_rule univ (make_act key tac) (make_vprod_item lev "tactic") prods in
   let _ = find_position true true None None (* to synchronise with remove *) in
-  grammar_extend entry pos [(None, None, List.rev rules)]
+  grammar_extend entry pos [(None, None, List.rev [rules])]
 
 let extend_grammar gram =
   (match gram with
   | Notation (_,a) -> extend_constr_notation a
   | Grammar g -> extend_grammar_rules g
-  | TacticGrammar (n,l) -> add_tactic_entries (n,l));
+  | TacticGrammar g -> add_tactic_entry g);
   grammar_state := gram :: !grammar_state
 
 let reset_extend_grammars_v8 () =
@@ -478,7 +469,7 @@ let reset_extend_grammars_v8 () =
 
 let recover_notation_grammar ntn prec =
   let l = map_succeed (function
-    | Notation (prec',(_,_,ntn',_,_ as x)) when prec = prec' & ntn = ntn' -> x
+    | Notation (prec',(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' -> x
     | _ -> failwith "") !grammar_state in
   assert (List.length l = 1);
   List.hd l
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 54e069512..06ab2b42f 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -21,16 +21,14 @@ open Mod_subst
 (*i*)
 
 type notation_grammar = 
-    int * Gramext.g_assoc option * notation * prod_item list * int list option
+    int * Gramext.g_assoc option * notation * prod_item list
 
 type all_grammar_command =
   | Notation of (precedence * tolerability list) * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
-      int *
-      (string * grammar_production list * 
-       (Names.dir_path * Tacexpr.glob_tactic_expr))
-      list
+      (string * int * grammar_production list * 
+        (Names.dir_path * Tacexpr.glob_tactic_expr))
 
 val extend_grammar : all_grammar_command -> unit
 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 70f28a278..21aa0c732 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -685,22 +685,22 @@ GEXTEND Gram
 	 op = ne_string; ":="; p = global; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         VernacInfix (local,(op,modl),p,None,sc)
+         VernacInfix (local,(op,modl),p,sc)
      | IDENT "Notation"; local = locality; id = ident; ":="; c = constr;
 	 b = [ "("; IDENT "only"; IDENT "parsing"; ")" -> true | -> false ] ->
            VernacSyntacticDefinition (id,c,local,b)
      | IDENT "Notation"; local = locality; s = ne_string; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (local,c,Some(s,modl),None,sc)
+           VernacNotation (local,c,(s,modl),sc)
 
      | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; 
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
-         -> VernacTacticGrammar (n,["",pil,t])
+         -> VernacTacticNotation (n,pil,t)
 
      | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (local,Some(s,l),None)
+	 -> VernacSyntaxExtension (local,(s,l))
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)