From 97e6e937433d52eba1ab01863d19db8bd85f2bc3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Jun 2016 01:02:33 +0200
Subject: Properly handle the only printing flag in Reserved Notations.

---
 toplevel/metasyntax.ml | 11 +++--------
 1 file changed, 3 insertions(+), 8 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 586d9f1cf8..e772ea0205 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -991,12 +991,7 @@ let compute_pure_syntax_data df mods =
       (Feedback.msg_warning ?loc:None,
       strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs
     else msgs in
-  let msgs =
-    if onlyprint then
-      (Feedback.msg_warning ?loc:None,
-      strbrk "The only printing modifier has no effect in Reserved Notation.")::msgs
-    else msgs in
-  msgs, sy_data, extra
+  msgs, sy_data, extra, onlyprint
 
 (**********************************************************************)
 (* Registration of notations interpretation                            *)
@@ -1213,8 +1208,8 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
 (* Notations without interpretation (Reserved Notation) *)
 
 let add_syntax_extension local ((loc,df),mods) =
-  let msgs, sy_data, extra = compute_pure_syntax_data df mods in
-  let sy_rules = make_syntax_rules sy_data extra false in
+  let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in
+  let sy_rules = make_syntax_rules sy_data extra onlyprint in
   Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
-- 
cgit v1.2.3