From 1c5e311d6a92deb66ba412c56516a4b71a513e01 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 20 Nov 2016 15:35:05 +0100
Subject: Fixing printing of "only parsing" in abbreviations.

---
 printing/ppvernac.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3494ad006f..be15879184 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1015,7 +1015,10 @@ module Make
             (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
                prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
                pr_syntax_modifiers
-               (match compat with None -> [] | Some v -> [SetCompatVersion v]))
+               (match compat with
+                | None -> []
+                | Some Flags.Current -> [SetOnlyParsing]
+                | Some v -> [SetCompatVersion v]))
         )
       | VernacDeclareImplicits (q,[]) ->
         return (
-- 
cgit v1.2.3