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
---
 intf/vernacexpr.mli | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 568d8a38ec..37f25e0ac4 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -122,9 +122,12 @@ type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type inductive_flag = Decl_kinds.recursivity_kind
-type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 type full_locality_flag = bool option (* true = Local; false = Global      *)
+type onlyparsing_flag = Flags.compat_version option
+ (* Some v = Parse only;  None = Print also.
+    If v<>Current, it contains the name of the coq version
+    which this notation is trying to be compatible with *)
 
 type option_value = Interface.option_value =
   | BoolValue of bool
@@ -183,7 +186,7 @@ type syntax_modifier =
   | SetLevel of int
   | SetAssoc of Compat.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
-  | SetOnlyParsing
+  | SetOnlyParsing of Flags.compat_version
   | SetFormat of string located
 
 type proof_end =
-- 
cgit v1.2.3