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

1 files changed, 13 insertions, 5 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fee4fef182..52722c9f5f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -770,7 +770,7 @@ let interp_modifiers modl =
     | SetAssoc a :: l ->
 	if assoc <> None then error"An associativity is given more than once.";
 	interp (Some a) level etyps format l
-    | SetOnlyParsing :: l ->
+    | SetOnlyParsing _ :: l ->
 	onlyparsing := true;
 	interp assoc level etyps format l
     | SetFormat s :: l ->
@@ -783,8 +783,13 @@ let check_infix_modifiers modifiers =
   if t <> [] then
     error "Explicit entry level or type unexpected in infix notation."
 
-let no_syntax_modifiers modifiers =
-  modifiers = [] or modifiers = [SetOnlyParsing]
+let no_syntax_modifiers = function
+  | [] | [SetOnlyParsing _] -> true
+  | _ -> false
+
+let is_only_parsing = function
+  | [SetOnlyParsing _] -> true
+  | _ -> false
 
 (* Compute precedences from modifiers (or find default ones) *)
 
@@ -1131,7 +1136,7 @@ let add_notation local c ((loc,df),modifiers) sc =
   let df' =
    if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
-    let onlyparse = modifiers=[SetOnlyParsing] in
+    let onlyparse = is_only_parsing modifiers in
     try add_notation_interpretation_core local df c sc onlyparse
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
@@ -1209,6 +1214,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       let vars,pat = interp_notation_constr i_vars [] c in
       List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
   in
-  let onlyparse = onlyparse or is_not_printable pat in
+  let onlyparse = match onlyparse with
+    | None when (is_not_printable pat) -> Some Flags.Current
+    | p -> p
+  in
   Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)