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
---
 lib/flags.ml  | 15 +++++++++++----
 lib/flags.mli |  5 +++--
 2 files changed, 14 insertions(+), 6 deletions(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index b4f6272acf..8cce04c50f 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -38,12 +38,19 @@ let record_print = ref true
 
 (* Compatibility mode *)
 
-type compat_version = V8_2 | V8_3
-let compat_version = ref None
-let version_strictly_greater v =
-  match !compat_version with None -> true | Some v' -> v'>v
+(* Current means no particular compatibility consideration.
+   For correct comparisons, this constructor should remain the last one. *)
+
+type compat_version = V8_2 | V8_3 | Current
+let compat_version = ref Current
+let version_strictly_greater v = !compat_version > v
 let version_less_or_equal v = not (version_strictly_greater v)
 
+let pr_version = function
+  | V8_2 -> "8.2"
+  | V8_3 -> "8.3"
+  | Current -> "current"
+
 (* Translate *)
 let beautify = ref false
 let make_beautify f = beautify := f
diff --git a/lib/flags.mli b/lib/flags.mli
index 77399b9e5e..0aceee0459 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -26,10 +26,11 @@ val load_proofs : load_proofs ref
 val raw_print : bool ref
 val record_print : bool ref
 
-type compat_version = V8_2 | V8_3
-val compat_version : compat_version option ref
+type compat_version = V8_2 | V8_3 | Current
+val compat_version : compat_version ref
 val version_strictly_greater : compat_version -> bool
 val version_less_or_equal : compat_version -> bool
+val pr_version : compat_version -> string
 
 val beautify : bool ref
 val make_beautify : bool -> unit
-- 
cgit v1.2.3