From 5520db62486ad628f91737833623aa69c4c1b8af Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 6 Jun 2016 20:16:32 +0200
Subject: Removing the use to Egramcoq.recover_constr_grammar.

---
 intf/notation_term.mli | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'intf')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index 7c5d7657be..c7c301629e 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -78,3 +78,18 @@ type notation_interp_env = {
   ninterp_rec_vars : Id.t Id.Map.t;
   mutable ninterp_only_parse : bool;
 }
+
+type grammar_constr_prod_item =
+  | GramConstrTerminal of Tok.t
+  | GramConstrNonTerminal of Extend.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 : Extend.gram_assoc option;
+  notgram_notation : Constrexpr.notation;
+  notgram_prods : grammar_constr_prod_item list list;
+  notgram_typs : notation_var_internalization_type list;
+}
-- 
cgit v1.2.3


From d7737ba9b3a811b8415ce87d8e3e091c9e49d32e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 6 Jun 2016 17:08:55 +0200
Subject: Adding an only printing flag to notations.

---
 intf/notation_term.mli | 1 +
 intf/vernacexpr.mli    | 1 +
 2 files changed, 2 insertions(+)

(limited to 'intf')

diff --git a/intf/notation_term.mli b/intf/notation_term.mli
index c7c301629e..883b017727 100644
--- a/intf/notation_term.mli
+++ b/intf/notation_term.mli
@@ -92,4 +92,5 @@ type notation_grammar = {
   notgram_notation : Constrexpr.notation;
   notgram_prods : grammar_constr_prod_item list list;
   notgram_typs : notation_var_internalization_type list;
+  notgram_onlyprinting : bool;
 }
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index ae9328fcc0..0e37f5268e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -206,6 +206,7 @@ type syntax_modifier =
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing of Flags.compat_version
+  | SetOnlyPrinting
   | SetFormat of string * string located
 
 type proof_end =
-- 
cgit v1.2.3