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

12 files changed, 90 insertions, 192 deletions

diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index a6a8937ba5..7728cf48ab 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -96,7 +96,6 @@ let execute_when_necessary ast =
 
 let execute_when_necessary v =
  (match v with
-  | VernacGrammar _ -> Vernacentries.interp v
   | VernacOpenCloseScope sc -> Vernacentries.interp v
   | VernacRequire (_,_,l) ->
       (try 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 69c6674d3a..54508443da 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1954,8 +1954,6 @@ let rec xlate_vernac =
       CT_require(ct_impexp, ct_spec, 
 		 CT_coerce_STRING_to_ID_NE_LIST_OR_STRING(CT_string filename))
 
-   | VernacSyntax (phylum, l) -> xlate_error "SYNTAX not implemented"
-
    | VernacOpenCloseScope(true, true, s) -> CT_local_open_scope(CT_ident s)
    | VernacOpenCloseScope(false, true, s) -> CT_open_scope(CT_ident s)
    | VernacOpenCloseScope(true, false, s) -> CT_local_close_scope(CT_ident s)
@@ -1977,8 +1975,7 @@ let rec xlate_vernac =
 		     CT_id_ne_list(xlate_class_rawexpr a,
 				   List.map xlate_class_rawexpr l))
    | VernacBindScope(id, []) -> assert false
-   | VernacNotation(b, c, None, _, _) -> assert false
-   | VernacNotation(b, c, Some(s,modif_list), _, opt_scope) -> 
+   | VernacNotation(b, c, (s,modif_list), opt_scope) -> 
        let translated_s = CT_string s in
        let formula = xlate_formula c in
        let translated_modif_list = 
@@ -1992,7 +1989,7 @@ let rec xlate_vernac =
        else
 	 CT_define_notation(translated_s, formula, 
 			    translated_modif_list, translated_scope)
-   | VernacSyntaxExtension(b,Some(s,modif_list), None) -> 
+   | VernacSyntaxExtension(b,(s,modif_list)) -> 
        let translated_s = CT_string s in
        let translated_modif_list = 
 	 CT_modifier_list(List.map xlate_syntax_modifier modif_list) in
@@ -2000,8 +1997,7 @@ let rec xlate_vernac =
 	 CT_local_reserve_notation(translated_s, translated_modif_list)
        else
 	 CT_reserve_notation(translated_s, translated_modif_list)
-   | VernacSyntaxExtension(_, _, _) -> assert false
-   | VernacInfix (b,(str,modl),id,_, opt_scope) ->
+   | VernacInfix (b,(str,modl),id, opt_scope) ->
        let id1 = loc_qualid_to_ct_ID id in
        let modl1 = CT_modifier_list(List.map xlate_syntax_modifier modl) in
        let s = CT_string str in
@@ -2012,7 +2008,6 @@ let rec xlate_vernac =
 	   CT_local_infix(s, id1,modl1, translated_scope)
 	 else
 	   CT_infix(s, id1,modl1, translated_scope)
-   | VernacGrammar _ -> xlate_error "GRAMMAR not implemented"
    | VernacCoercion (s, id1, id2, id3) ->
       let id_opt = CT_coerce_NONE_to_IDENTITY_OPT CT_none in
       let local_opt =
@@ -2126,8 +2121,8 @@ let rec xlate_vernac =
   | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)
   | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _|
-    VernacSolveExistential (_, _)|VernacCanonical _ | VernacDistfix _|
-     VernacTacticGrammar _)
+    VernacSolveExistential (_, _)|VernacCanonical _ |
+     VernacTacticNotation _)
     -> xlate_error "TODO: vernac";;
 
 let rec xlate_vernac_list =
diff --git a/interp/notation.ml b/interp/notation.ml
index 7874f95b38..f116f292c3 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -44,7 +44,7 @@ type level = precedence * tolerability list
 type delimiters = string
 
 type scope = {
-  notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
+  notations: (interpretation * (dir_path * string)) Stringmap.t;
   delimiters: delimiters option
 }
 
@@ -270,13 +270,13 @@ let level_of_notation ntn =
 
 (* The mapping between notations and their interpretation *)
 
-let declare_notation_interpretation ntn scopt pat df pp8only =
+let declare_notation_interpretation ntn scopt pat df =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   if Stringmap.mem ntn sc.notations && Options.is_verbose () then
     warning ("Notation "^ntn^" was already used"^
     (if scopt = None then "" else " in scope "^scope));
-  let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in
+  let sc = { sc with notations = Stringmap.add ntn (pat,df) sc.notations } in
   scope_map := Stringmap.add scope sc !scope_map;
   if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
 
@@ -296,8 +296,7 @@ let rec find_interpretation f = function
 let rec interp_notation loc ntn scopes =
   let f sc =
     let scope = find_scope sc in
-    let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
-    if pp8only then raise Not_found;
+    let (pat,df) = Stringmap.find ntn scope.notations in
     pat,(df,if sc = default_scope then None else Some sc) in
   try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
   with Not_found -> 
@@ -361,9 +360,9 @@ let exists_notation_in_scope scopt ntn r =
   let scope = match scopt with Some s -> s | None -> default_scope in
   try
     let sc = Stringmap.find scope !scope_map in
-    let (r',_,pp8only) = Stringmap.find ntn sc.notations in
-    r' = r, pp8only
-  with Not_found -> false, false
+    let (r',_) = Stringmap.find ntn sc.notations in
+    r' = r
+  with Not_found -> false
 
 (**********************************************************************)
 (* Mapping classes to scopes *)
@@ -506,7 +505,7 @@ let pr_named_scope prraw scope sc =
   ++ fnl ()
   ++ pr_scope_classes scope
   ++ Stringmap.fold
-       (fun ntn ((_,r),(_,df),_) strm ->
+       (fun ntn ((_,r),(_,df)) strm ->
 	 pr_notation_info prraw df r ++ fnl () ++ strm)
        sc.notations (mt ())
 
@@ -544,7 +543,7 @@ let browse_notation ntn map =
   let l =
     Stringmap.fold 
       (fun scope_name sc ->
-	Stringmap.fold (fun ntn ((_,r),df,_) l ->
+	Stringmap.fold (fun ntn ((_,r),df) l ->
 	  if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations)
       map [] in
   let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in
@@ -572,7 +571,7 @@ let locate_notation prraw ntn =
 let collect_notation_in_scope scope sc known =
   assert (scope <> default_scope);
   Stringmap.fold
-    (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
+    (fun ntn ((_,r),(_,df)) (l,known as acc) ->
       if List.mem ntn known then acc else ((df,r)::l,ntn::known))
     sc.notations ([],known)
 
@@ -588,7 +587,7 @@ let collect_notations stack =
       | SingleNotation ntn ->
 	  if List.mem ntn knownntn then (all,knownntn)
 	  else
-	    let ((_,r),(_,df),_) =
+	    let ((_,r),(_,df)) =
 	      Stringmap.find ntn (find_scope default_scope).notations in
 	    let all' = match all with
 	      | (s,lonelyntn)::rest when s = default_scope ->
diff --git a/interp/notation.mli b/interp/notation.mli
index 0e401acd6e..896d427932 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -88,7 +88,7 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
 val declare_notation_interpretation : notation -> scope_name option ->
-      interpretation -> dir_path * string -> bool -> unit
+      interpretation -> dir_path * string -> unit
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
@@ -111,15 +111,14 @@ val availability_of_notation : scope_name option * notation -> scopes ->
 
 (*s Declare and test the level of a (possibly uninterpreted) notation *)
 
-val declare_notation_level : notation -> level option * level -> unit
-val level_of_notation : notation -> level option * level 
-      (* raise [Not_found] if no level *)
+val declare_notation_level : notation -> level -> unit
+val level_of_notation : notation -> level (* raise [Not_found] if no level *)
 
 (*s** Miscellaneous *)
 
 (* Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
-      interpretation -> bool * bool
+      interpretation -> bool
 
 (* Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope: global_reference -> scope_name option list -> unit
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index e0d877b66e..be8b1e8ad8 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 54e0695123..06ab2b42fb 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 70f28a2787..21aa0c732d 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 *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 8d4f3b83f4..24bee11e12 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -88,19 +88,15 @@ let rec make_tags lev = function
       etyp :: make_tags lev l
   | [] -> []
 
-let declare_tactic_pprule n (s,t,p) =
-  Pptactic.declare_extra_tactic_pprule true s (t,p);
-  Pptactic.declare_extra_tactic_pprule false s (t,p)
+let cache_tactic_notation (_,(pa,pp)) =
+  Egrammar.extend_grammar (Egrammar.TacticGrammar pa);
+  Pptactic.declare_extra_tactic_pprule true (pi1 pp) (pi2 pp, pi3 pp)
 
-let cache_tactic_notation (_,((n,pa),pp)) =
-  Egrammar.extend_grammar (Egrammar.TacticGrammar (n,pa));
-  List.iter (declare_tactic_pprule n) pp
+let subst_tactic_parule subst (key,n,p,(d,tac)) =
+  (key,n,p,(d,Tacinterp.subst_tactic subst tac))
 
-let subst_one_tactic_notation subst (s,p,(d,tac)) =
-  (s,p,(d,Tacinterp.subst_tactic subst tac))
-
-let subst_tactic_notation (_,subst,((n,pa),pp)) =
-  ((n,List.map (subst_one_tactic_notation subst) pa),pp)
+let subst_tactic_notation (_,subst,(pa,pp)) =
+  (subst_tactic_parule subst pa,pp)
 
 let (inTacticGrammar, outTacticGrammar) =
   declare_object {(default_object "TacticGrammar") with
@@ -123,23 +119,14 @@ let rec next_key_away key t =
   if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
   else key
 
-let make_tactic_pprule n s prods =
+let add_tactic_notation (n,prods,e) =
   let tags = make_tags n prods in
-  let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in
-  (s, tags, (n,List.map make_terminal_status prods))
-
-let make_tactic_parule s prods e =
+  let key = next_key_away (tactic_notation_key prods) tags in
+  let pprule = (key,tags,(n,List.map make_terminal_status prods)) in
   let ids = List.fold_left cons_production_parameter [] prods in
   let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
-  (s,prods,(Lib.cwd (),tac))
-
-let locate_tactic_body n (s,prods,e) =
-  let (s',t,p as pp) = make_tactic_pprule n s prods in
-  (make_tactic_parule s' prods e, pp)
-
-let add_tactic_notation (n,g) =
-  let pa,pp = List.split (List.map (locate_tactic_body n) g) in
-  Lib.add_anonymous_leaf (inTacticGrammar ((n,pa),pp))
+  let parule = (key,n,prods,(Lib.cwd(),tac)) in
+  Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule))
 
 (**********************************************************************)
 (* Printing grammar entries                                           *)
@@ -631,7 +618,7 @@ let recompute_assoc typs =
 let make_grammar_rule (n,typs,symbols,_) ntn =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
-  (n,assoc,ntn,prod,None)
+  (n,assoc,ntn,prod)
 
 let make_pp_rule (n,typs,symbols,fmt) =
   match fmt with
@@ -654,7 +641,7 @@ let pr_level ntn (from,args) =
 
 let cache_syntax_extension (_,(_,(prec,ntn,gr,pp))) =
   try 
-    let _, oldprec = Notation.level_of_notation ntn in
+    let oldprec = Notation.level_of_notation ntn in
     if prec <> oldprec then
       errorlabstrm ""
 	(str ("Notation "^ntn^" is already defined") ++ spc() ++ 
@@ -663,7 +650,7 @@ let cache_syntax_extension (_,(_,(prec,ntn,gr,pp))) =
 	 pr_level ntn prec);
   with Not_found ->
     (* Reserve the notation level *)
-    Notation.declare_notation_level ntn (None,prec);
+    Notation.declare_notation_level ntn prec;
     (* Declare the parsing rule *)
     Egrammar.extend_grammar (Egrammar.Notation (prec,gr));
     (* Declare the printing rule *)
@@ -869,10 +856,10 @@ let load_notation _ (_,(_,scope,pat,onlyparse,_)) =
 
 let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) =
   if i=1 then begin
-    let exists,_ = Notation.exists_notation_in_scope scope ntn pat in
+    let exists = Notation.exists_notation_in_scope scope ntn pat in
     (* Declare the interpretation *)
     if not exists then
-      Notation.declare_notation_interpretation ntn scope pat df false;
+      Notation.declare_notation_interpretation ntn scope pat df;
     if not exists & not onlyparse then
       Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat
   end
@@ -929,7 +916,7 @@ let level_rule (n,p) = if p = E then n else max (n-1) 0
 
 let recover_syntax ntn = 
   try 
-    let _,prec = Notation.level_of_notation ntn in
+    let prec = Notation.level_of_notation ntn in
     let pprule,_ = Notation.find_notation_printing_rule ntn in
     let gr = Egrammar.recover_notation_grammar ntn prec in
     Some (prec,ntn,gr,pprule)
@@ -1022,7 +1009,7 @@ let add_infix local (inf,modl) pr sc =
   else
     add_notation_in_scope local df a modl sc toks
 
-let standardise_locatable_notation ntn =
+let standardize_locatable_notation ntn =
   let unquote = function
     | String s -> [unquote_notation_token s]
     | _ -> [] in
@@ -1070,16 +1057,3 @@ let add_delimiters scope key =
 
 let add_class_scope scope cl = 
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
-
-
-(* Temporary compatibility *)
-
-let translate_distfix _ = failwith "No more v7 support 1"
-let add_distfix _ = failwith "No more v7 support 2"
-let add_tactic_grammar = add_tactic_notation
-let add_grammar_obj _ = failwith "No more v7 support 4"
-let add_syntax_obj _ = failwith "No more v7 support 5"
-
-let add_syntax_extension local mv _ = add_syntax_extension local (out_some mv)
-let add_notation local c x _ sc = add_notation local c (out_some x) sc
-let add_infix local x pr _ sc = add_infix local x pr sc
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 243b6345fd..869ba00d0f 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -19,38 +19,27 @@ open Notation
 open Topconstr
 (*i*)
 
-(* Adding grammar and pretty-printing objects in the environment *)
+(* Adding parsing and pretty-printing rules in the environment *)
 
-val add_syntax_obj : string -> raw_syntax_entry list -> unit
-
-val add_grammar_obj : string -> raw_grammar_entry list -> unit
 val add_token_obj : string -> unit
-val add_tactic_grammar : 
-  int * (string * grammar_production list * raw_tactic_expr) list -> unit
+
+val add_tactic_notation : 
+  int * grammar_production list * raw_tactic_expr -> unit
 
 val add_infix : locality_flag -> (string * syntax_modifier list) ->
-  reference -> (string * syntax_modifier list) option ->
-    scope_name option -> unit
-val add_distfix : locality_flag ->
-  grammar_associativity -> precedence -> string -> reference
-    -> scope_name option -> unit
-val translate_distfix : grammar_associativity -> string -> reference ->
-  Gramext.g_assoc * string * constr_expr
+  reference -> scope_name option -> unit
 
 val add_delimiters : scope_name -> string -> unit
 val add_class_scope : scope_name -> Classops.cl_typ -> unit
 
-val add_notation : locality_flag -> constr_expr
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option
-      -> scope_name option -> unit
+val add_notation : locality_flag -> constr_expr ->
+  (string * syntax_modifier list) -> scope_name option -> unit
 
-val add_notation_interpretation : string -> Constrintern.implicits_env
-  -> constr_expr -> scope_name option -> unit
+val add_notation_interpretation : string -> Constrintern.implicits_env ->
+  constr_expr -> scope_name option -> unit
 
-val add_syntax_extension : locality_flag
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option -> unit
+val add_syntax_extension : 
+  locality_flag -> (string * syntax_modifier list) -> unit
 
 val print_grammar : string -> string -> unit
 
@@ -60,4 +49,4 @@ val merge_modifiers : Gramext.g_assoc option -> int option ->
 val interp_infix_modifiers : syntax_modifier list ->
   Gramext.g_assoc option * precedence option * bool * string located option
 
-val standardise_locatable_notation : string -> string
+val standardize_locatable_notation : string -> string
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index a93e6fd5e6..fb9bb44967 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -280,10 +280,6 @@ let print_located_module r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax = Metasyntax.add_syntax_obj
-
-let vernac_grammar = Metasyntax.add_grammar_obj
-
 let vernac_syntax_extension = Metasyntax.add_syntax_extension
 
 let vernac_delimiters = Metasyntax.add_delimiters
@@ -298,8 +294,6 @@ let vernac_arguments_scope qid scl =
 
 let vernac_infix = Metasyntax.add_infix
 
-let vernac_distfix = Metasyntax.add_distfix
-
 let vernac_notation = Metasyntax.add_notation
 
 (***********)
@@ -974,7 +968,7 @@ let vernac_locate = function
   | LocateFile f -> locate_file f
   | LocateNotation ntn ->
       ppnl (Notation.locate_notation (Constrextern.without_symbols pr_rawterm)
-	(Metasyntax.standardise_locatable_notation ntn))
+	(Metasyntax.standardize_locatable_notation ntn))
 
 (********************)
 (* Proof management *)
@@ -1108,19 +1102,14 @@ let interp c = match c with
   | (VernacV7only _ | VernacV8only _) -> assert false
 
   (* Syntax *)
-  | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
-  | VernacTacticGrammar (n,al) -> Metasyntax.add_tactic_grammar (n,al)
-  | VernacGrammar (univ,al) -> vernac_grammar univ al
-  | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8
+  | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e)
+  | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope sc -> vernac_open_close_scope sc
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
-  | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc
-  | VernacDistfix (local,assoc,n,inf,qid,sc) -> 
-      vernac_distfix local assoc n inf qid sc
-  | VernacNotation (local,c,infpl,mv8,sc) ->
-      vernac_notation local c infpl mv8 sc
+  | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
+  | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
 
   (* Gallina *)
   | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index e62288d16d..ab05f7d0df 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -172,25 +172,17 @@ type vernac_expr =
   | VernacVar of lident
 
   (* Syntax *) 
-  | VernacGrammar of lstring * raw_grammar_entry list
-  | VernacTacticGrammar of int *
-      (lstring * grammar_production list * raw_tactic_expr) list
-  | VernacSyntax of lstring * raw_syntax_entry list
-  | VernacSyntaxExtension of locality_flag *
-      (lstring * syntax_modifier list) option 
-      * (lstring * syntax_modifier list) option
-  | VernacDistfix of locality_flag *
-      grammar_associativity * precedence * lstring * lreference *
-      scope_name option
+  | VernacTacticNotation of int * grammar_production list * raw_tactic_expr
+  | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * lstring
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacArgumentsScope of lreference * scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
-      lreference * (lstring * syntax_modifier list) option * scope_name option
+      lreference * scope_name option
   | VernacNotation of
-      locality_flag * constr_expr * (lstring * syntax_modifier list) option *
-      (lstring * syntax_modifier list) option * scope_name option
+      locality_flag * constr_expr * (lstring * syntax_modifier list) *
+      scope_name option
 
   (* Gallina *)
   | VernacDefinition of definition_kind * lident * definition_expr * 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 154d23c38d..77b523333f 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -403,7 +403,7 @@ let pr_syntax_modifiers = function
 let print_level n =
   if n <> 0 then str " (at level " ++ int n ++ str ")" else mt ()
 
-let pr_grammar_tactic_rule n (name,pil,t) =
+let pr_grammar_tactic_rule n (_,pil,t) =
   hov 2 (str "Tactic Notation" ++ print_level n ++ spc() ++ 
     hov 0 (prlist_with_sep sep pr_production_item pil ++
     spc() ++ str":=" ++ spc() ++ pr_raw_tactic t))
@@ -520,21 +520,7 @@ let rec pr_vernac = function
   | VernacVar id -> pr_lident id
   
   (* Syntax *) 
-  | VernacGrammar _ -> 
-      msgerrnl (str"Warning : constr Grammar is discontinued; use Notation");
-      str"(* <Warning> : Grammar is replaced by Notation *)"
-  | VernacTacticGrammar (n,l) ->
-      prlist_with_sep (fun () -> sep_end() ++ fnl())
-        (pr_grammar_tactic_rule n) l
-  | VernacSyntax (u,el) ->
-      msgerrnl (str"Warning : Syntax is discontinued; use Notation");
-      str"(* <Warning> : Syntax is discontinued" ++ 
-(*
-      fnl () ++
-      hov 1 (str"Syntax " ++ str u ++ spc() ++
-      prlist_with_sep sep_v2 pr_syntax_entry el) ++ 
-*)
-      str " *)"
+  | VernacTacticNotation (n,r,e) -> pr_grammar_tactic_rule n ("",r,e)
   | VernacOpenCloseScope (local,opening,sc) ->
       str (if opening then "Open " else "Close ") ++ pr_locality local ++
       str "Scope" ++ spc() ++ str sc
@@ -548,23 +534,14 @@ let rec pr_vernac = function
       |	None -> str"_"
       |	Some sc -> str sc in 
     str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
-  | VernacInfix (local,(s,_),q,ov8,sn) -> (* A Verifier *)
-      let s,mv8 = match ov8 with Some smv8 -> smv8 | None -> (s,[]) in
+  | VernacInfix (local,(s,mv),q,sn) -> (* A Verifier *)
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
       ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++
-      pr_syntax_modifiers mv8 ++
+      pr_syntax_modifiers mv ++
       (match sn with
     | None -> mt()
     | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
-  | VernacDistfix (local,a,p,s,q,sn) ->
-      hov 0 (str"Distfix " ++ pr_locality local ++ pr_entry_prec a ++ int p
-        ++ spc() ++ qsnew s ++ spc() ++ pr_reference q ++ (match sn with
-    | None -> mt()
-    | Some sc -> spc() ++ str":" ++ spc() ++ str sc))
-  | VernacNotation (local,c,sl,mv8,opt) ->
-      let (s,l) = match mv8 with
-          None -> fst (out_some sl), []
-        | Some ml -> ml in
+  | VernacNotation (local,c,(s,l),opt) ->
       let ps =
 	let n = String.length s in
 	if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' 
@@ -577,10 +554,7 @@ let rec pr_vernac = function
       (match opt with
         | None -> mt()
         | Some sc -> str" :" ++ spc() ++ str sc))
-  | VernacSyntaxExtension (local,sl,mv8) ->
-      let (s,l) = match mv8 with
-          None -> out_some sl
-        | Some ml -> ml in
+  | VernacSyntaxExtension (local,(s,l)) ->
       str"Reserved Notation" ++ spc() ++ pr_locality local ++ qsnew s ++
       pr_syntax_modifiers l
 
@@ -1132,7 +1106,6 @@ let pr_vernac = function
       (* Pour ceux qui ont utilisé la couche "Import *_scope" de compat *)
       let a = Names.string_of_id a in
       a = "nat_scope" or a = "Z_scope" or a = "R_scope" -> mt()
-  | VernacSyntax _  | VernacGrammar _ as x -> pr_vernac x
   | VernacPrint PrintLocalContext -> 
       warning ("\"Print.\" is discontinued");
       mt ()