From f93f073df630bb46ddd07802026c0326dc72dafd Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 Jul 2012 16:55:59 +0000
Subject: Notation: a new annotation "compat 8.x" extending "only parsing"

 Suppose we declare : Notation foo := bar (compat "8.3").
 Then each time foo is used in a script :

 - By default nothing particular happens (for the moment)

 - But we could get a warning explaining that
   "foo is bar since coq > 8.3".
   For that, either use the command-line option -verb-compat-notations
   or the interactive command "Set Verbose Compat Notations".

 - There is also a strict mode, where foo is forbidden : the previous
   warning is now an error.
   For that, either use the command-line option -no-compat-notations
   or the interactive command "Unset Compat Notations".

 When Coq is launched in compatibility mode (via -compat 8.x),
 using a notation tagged "8.x" will never trigger a warning or error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 printing/ppvernac.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 9513001f47..d7b36d2878 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -381,7 +381,8 @@ let pr_syntax_modifier = function
   | SetAssoc RightA -> str"right associativity"
   | SetAssoc NonA -> str"no associativity"
   | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
-  | SetOnlyParsing -> str"only parsing"
+  | SetOnlyParsing Flags.Current -> str"only parsing"
+  | SetOnlyParsing v -> str("compat \"" ^ Flags.pr_version v ^ "\"")
   | SetFormat s -> str"format " ++ pr_located qs s
 
 let pr_syntax_modifiers = function
@@ -779,7 +780,8 @@ let rec pr_vernac = function
       hov 2
         (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++
 	 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
-         pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
+         pr_syntax_modifiers
+	   (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
   | VernacDeclareImplicits (local,q,[]) ->
       hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++
 	pr_smart_global q)
-- 
cgit v1.2.3