Merge remote-tracking branch 'github/pr/194' into trunk

3 files changed, 4 insertions, 47 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 21a9afa293..ade31c1d3c 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -9,9 +9,10 @@
 open Errors
 open Util
 open Pcoq
-open Extend
 open Constrexpr
+open Notation
 open Notation_term
+open Extend
 open Libnames
 open Names
 
@@ -320,13 +321,6 @@ let cases_pattern_expr_of_name (loc,na) = match na with
   | Anonymous -> CPatAtom (loc,None)
   | Name id -> CPatAtom (loc,Some (Ident (loc,id)))
 
-type grammar_constr_prod_item =
-  | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
-  | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items;
-       concat with last parsed list if true *)
-
 type 'r env = {
   constrs : 'r list;
   constrlists : 'r list list;
@@ -444,14 +438,6 @@ let make_act : type r. r target -> _ -> r gen_eval = function
   let env = (env.constrs, env.constrlists) in
   CPatNotation (loc, notation, env, [])
 
-type notation_grammar = {
-  notgram_level : int;
-  notgram_assoc : gram_assoc option;
-  notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
-}
-
 let extend_constr state forpat ng =
   let n = ng.notgram_level in
   let assoc = ng.notgram_assoc in
@@ -491,12 +477,3 @@ let constr_grammar : (Notation.level * notation_grammar) grammar_command =
   create_grammar_command "Notation" extend_constr_notation
 
 let extend_constr_grammar pr ntn = extend_grammar_command constr_grammar (pr, ntn)
-
-let recover_constr_grammar ntn prec =
-  let filter (prec', ng) =
-    if Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation then Some ng
-    else None
-  in
-  match List.map_filter filter (recover_grammar_command constr_grammar) with
-  | [x] -> x
-  | _ -> assert false
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 1fe06a29df..6dda3817ae 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -19,28 +19,7 @@ open Egramml
 (** This is the part specific to Coq-level Notation and Tactic Notation.
     For the ML-level tactic and vernac extensions, see Egramml. *)
 
-(** For constr notations *)
-
-type grammar_constr_prod_item =
-  | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of constr_prod_entry_key * Id.t option
-  | GramConstrListMark of int * bool
-    (* tells action rule to make a list of the n previous parsed items;
-       concat with last parsed list if true *)
-
-type notation_grammar = {
-  notgram_level : int;
-  notgram_assoc : gram_assoc option;
-  notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list;
-  notgram_typs : notation_var_internalization_type list;
-}
-
 (** {5 Adding notations} *)
 
-val extend_constr_grammar : Notation.level -> notation_grammar -> unit
+val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
-
-val recover_constr_grammar : notation -> Notation.level -> notation_grammar
-(** For a declared grammar, returns the rule + the ordered entry types
-    of variables in the rule (for use in the interpretation) *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0df15babd1..9c1f5afb86 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1076,6 +1076,7 @@ GEXTEND Gram
       | IDENT "left"; IDENT "associativity" -> SetAssoc LeftA
       | IDENT "right"; IDENT "associativity" -> SetAssoc RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc NonA
+      | IDENT "only"; IDENT "printing" -> SetOnlyPrinting
       | IDENT "only"; IDENT "parsing" ->
         SetOnlyParsing Flags.Current
       | IDENT "compat"; s = STRING ->