Remove deprecated compat modifier of Notation / Infix commands.

And simplify a lot the compatibility infrastructure following this.

Update dev/tools/update-compat.py

Remove much complexity.

Co-authored-by: Jason Gross <jgross@mit.edu>

12 files changed, 39 insertions, 229 deletions

diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 7312c2a5af..ddb0362186 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -15,10 +15,8 @@ from io import open
 #   [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
 #   with the deleted file.
 # - Remove any notations in the standard library which have `compat "U.U"`.
-# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
-#   bumping all the version numbers by one, and update the interpretations
-#   of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
-#   [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml)
+#   by bumping all the version numbers by one.
 #
 # - Remove the file
 #   [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v).
@@ -38,10 +36,8 @@ from io import open
 # - Update
 #   [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
 #   with the added file.
-# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by
-#   bumping all the version numbers by one, and update the interpretations
-#   of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and
-#   [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg).
+# - Update the function `get_compat_file` in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml)
+#   by bumping all the version numbers by one.
 # - Update the files
 #   [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
 #   [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
@@ -70,10 +66,7 @@ DEFAULT_NUMBER_OF_OLD_VERSIONS = 2
 RELEASE_NUMBER_OF_OLD_VERSIONS = 2
 MASTER_NUMBER_OF_OLD_VERSIONS = 3
 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n'
-FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli')
-FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml')
 COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
-G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
@@ -248,118 +241,38 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
                     contents = contents.replace(header, '%s\n%s' % (header, line))
                     update_file(contents, compat_path, exn_string=('Compat file %%s is missing line %s' % line), assert_unchanged=assert_unchanged, **args)
 
-def update_compat_versions_type_line(new_versions, contents, relpath):
-    compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current'])
-    new_compat_line = 'type compat_version = %s' % compat_version_string
-    new_contents = re.sub(r'^type compat_version = .*$', new_compat_line, contents, flags=re.MULTILINE)
-    if new_compat_line not in new_contents:
-        raise Exception("Could not find 'type compat_version =' in %s" % relpath)
-    return new_contents
-
-def update_version_compare(new_versions, contents, relpath):
-    first_line = 'let version_compare v1 v2 = match v1, v2 with'
-    new_lines = [first_line]
-    for v in new_versions[:-1]:
-        V = 'V%s_%s' % tuple(v.split('.'))
-        new_lines.append('  | %s, %s -> 0' % (V, V))
-        new_lines.append('  | %s, _ -> -1' % V)
-        new_lines.append('  | _, %s -> 1' % V)
-    new_lines.append('  | Current, Current -> 0')
-    new_lines = '\n'.join(new_lines)
-    new_contents = re.sub(first_line + '.*' + 'Current, Current -> 0', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
-    if new_lines not in new_contents:
-        raise Exception('Could not find version_compare in %s' % relpath)
-    return new_contents
-
-def update_pr_version(new_versions, contents, relpath):
-    first_line = 'let pr_version = function'
-    new_lines = [first_line]
-    for v in new_versions[:-1]:
-        V = 'V%s_%s' % tuple(v.split('.'))
-        new_lines.append('  | %s -> "%s"' % (V, v))
-    new_lines.append('  | Current -> "current"')
-    new_lines = '\n'.join(new_lines)
-    new_contents = re.sub(first_line + '.*' + 'Current -> "current"', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
-    if new_lines not in new_contents:
-        raise Exception('Could not find pr_version in %s' % relpath)
-    return new_contents
-
-def update_add_compat_require(new_versions, contents, relpath):
-    first_line = 'let add_compat_require opts v ='
-    new_lines = [first_line, '  match v with']
-    for v in new_versions[:-1]:
-        V = 'V%s_%s' % tuple(v.split('.'))
-        new_lines.append('  | Flags.%s -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % (V, version_name_to_compat_name(v, ext='')))
-    new_lines.append('  | Flags.Current -> add_vo_require opts "Coq.Compat.%s" None (Some false)' % version_name_to_compat_name(new_versions[-1], ext=''))
-    new_lines = '\n'.join(new_lines)
-    new_contents = re.sub(first_line + '.*' + 'Flags.Current -> add_vo_require opts "Coq.Compat.[^"]+" None .Some false.', new_lines, contents, flags=re.DOTALL|re.MULTILINE)
-    if new_lines not in new_contents:
-        raise Exception('Could not find add_compat_require in %s' % relpath)
-    return new_contents
-
-def update_parse_compat_version(new_versions, contents, relpath, **args):
+def update_get_compat_file(new_versions, contents, relpath):
     line_count = 3 # 1 for the first line, 1 for the invalid flags, and 1 for Current
-    first_line = 'let parse_compat_version = let open Flags in function'
+    first_line = 'let get_compat_file = function'
     split_contents = contents[contents.index(first_line):].split('\n')
     while True:
         cur_line = split_contents[:line_count][-1]
         if re.match(r'^  \| \([0-9 "\.\|]*\) as s ->$', cur_line) is not None:
             break
-        elif re.match(r'^  \| "[0-9\.]*" -> V[0-9_]*$', cur_line) is not None:
+        elif re.match(r'^  \| "[0-9\.]*" -> "Coq.Compat.Coq[0-9]*"$', cur_line) is not None:
             line_count += 1
         else:
-            raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line)))
+            raise Exception('Could not recognize line %d of get_compat_file in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line)))
     old_function_lines = split_contents[:line_count]
     all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines))
     invalid_versions = tuple(i for i in all_versions if i not in new_versions)
     new_function_lines = [first_line]
-    for v, V in reversed(list(zip(new_versions, ['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']))):
+    for v, V in reversed(list(zip(new_versions, ['"Coq.Compat.Coq%s%s"' % tuple(v.split('.')) for v in new_versions]))):
         new_function_lines.append('  | "%s" -> %s' % (v, V))
     new_function_lines.append('  | (%s) as s ->' % ' | '.join('"%s"' % v for v in invalid_versions))
     new_lines = '\n'.join(new_function_lines)
     new_contents = contents.replace('\n'.join(old_function_lines), new_lines)
     if new_lines not in new_contents:
-        raise Exception('Could not find parse_compat_version in %s' % relpath)
+        raise Exception('Could not find get_compat_file in %s' % relpath)
     return new_contents
 
-def check_no_old_versions(old_versions, new_versions, contents, relpath):
-    for v in old_versions:
-        if v not in new_versions:
-            V = 'V%s_%s' % tuple(v.split('.'))
-            if V in contents:
-                raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
-
-def update_flags_mli(old_versions, new_versions, **args):
-    contents = get_file(FLAGS_MLI_PATH)
-    new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
-    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
-    update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args)
-
-def update_flags_ml(old_versions, new_versions, **args):
-    contents = get_file(FLAGS_ML_PATH)
-    new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
-    new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
-    new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
-    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH))
-    update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args)
-
 def update_coqargs_ml(old_versions, new_versions, **args):
     contents = get_file(COQARGS_ML_PATH)
-    new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
-    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
+    new_contents = update_get_compat_file(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH))
     update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
 
-def update_g_vernac(old_versions, new_versions, **args):
-    contents = get_file(G_VERNAC_PATH)
-    new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args)
-    check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH))
-    update_if_changed(contents, new_contents, G_VERNAC_PATH, **args)
-
 def update_flags(old_versions, new_versions, **args):
-    update_flags_mli(old_versions, new_versions, **args)
-    update_flags_ml(old_versions, new_versions, **args)
     update_coqargs_ml(old_versions, new_versions, **args)
-    update_g_vernac(old_versions, new_versions, **args)
 
 def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, test_suite_outdated_paths=tuple(), **args):
     assert(len(new_versions) == len(test_suite_paths))
diff --git a/doc/changelog/03-notations/11113-remove-compat.rst b/doc/changelog/03-notations/11113-remove-compat.rst
new file mode 100644
index 0000000000..8c71d70cda
--- /dev/null
+++ b/doc/changelog/03-notations/11113-remove-compat.rst
@@ -0,0 +1,4 @@
+- Removed deprecated ``compat`` modifier of :cmd:`Notation`
+  and :cmd:`Infix` commands
+  (`#11113 <https://github.com/coq/coq/pull/11113>`_,
+  by Théo Zimmermann, with help from Jason Gross).
diff --git a/lib/flags.ml b/lib/flags.ml
index 27ca8e9596..b87ba46634 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -57,36 +57,6 @@ let raw_print = ref false
 
 let we_are_parsing = ref false
 
-(* Compatibility mode *)
-
-(* Current means no particular compatibility consideration.
-   For correct comparisons, this constructor should remain the last one. *)
-
-type compat_version = V8_9 | V8_10 | V8_11 | Current
-
-let compat_version = ref Current
-
-let version_compare v1 v2 = match v1, v2 with
-  | V8_9, V8_9 -> 0
-  | V8_9, _ -> -1
-  | _, V8_9 -> 1
-  | V8_10, V8_10 -> 0
-  | V8_10, _ -> -1
-  | _, V8_10 -> 1
-  | V8_11, V8_11 -> 0
-  | V8_11, _ -> -1
-  | _, V8_11 -> 1
-  | Current, Current -> 0
-
-let version_strictly_greater v = version_compare !compat_version v > 0
-let version_less_or_equal v = not (version_strictly_greater v)
-
-let pr_version = function
-  | V8_9 -> "8.9"
-  | V8_10 -> "8.10"
-  | V8_11 -> "8.11"
-  | Current -> "current"
-
 (* Translate *)
 let beautify = ref false
 let beautify_file = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 36a996401d..86a922847f 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -14,7 +14,7 @@
 
     This file is own its way to deprecation in favor of a purely
    functional state, but meanwhile it will contain options that are
-   truly global to the system such as [compat] or [debug]
+   truly global to the system such as [debug]
 
     If you are thinking about adding a global flag, well, just
    don't. First of all, options make testins exponentially more
@@ -52,13 +52,6 @@ val we_are_parsing : bool ref
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref
 
-type compat_version = V8_9 | V8_10 | V8_11 | Current
-val compat_version : compat_version ref
-val version_compare : compat_version -> compat_version -> int
-val version_strictly_greater : compat_version -> bool
-val version_less_or_equal : compat_version -> bool
-val pr_version : compat_version -> string
-
 (* Beautify command line flags, should move to printing? *)
 val beautify : bool ref
 val beautify_file : bool ref
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
index 96814a1b97..60d40d3d12 100644
--- a/test-suite/success/NotationDeprecation.v
+++ b/test-suite/success/NotationDeprecation.v
@@ -3,19 +3,11 @@ Module Syndefs.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Notation foo := Prop.
 
-Notation bar := Prop (compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Notation zar := Prop (compat "8.9").
-
 Check foo.
-Check bar.
 
 Set Warnings "+deprecated".
 
 Fail Check foo.
-Fail Check bar.
 
 End Syndefs.
 
@@ -24,19 +16,11 @@ Module Notations.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Notation "!!" := Prop.
 
-Notation "##" := Prop (compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Notation "**" := Prop (compat "8.9").
-
 Check !!.
-Check ##.
 
 Set Warnings "+deprecated".
 
 Fail Check !!.
-Fail Check ##.
 
 End Notations.
 
@@ -45,18 +29,10 @@ Module Infix.
 #[deprecated(since = "8.9", note = "Do not use.")]
 Infix "!!" := plus (at level 1).
 
-Infix "##" := plus (at level 1, compat "8.9").
-
-Fail
-#[deprecated(since = "8.9", note = "Do not use.")]
-Infix "**" := plus (at level 1, compat "8.9").
-
 Check (_ !! _).
-Check (_ ## _).
 
 Set Warnings "+deprecated".
 
 Fail Check (_ !! _).
-Fail Check (_ ## _).
 
 End Infix.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index e3116550d9..5326ce6114 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -174,13 +174,6 @@ let add_vo_include opts unix_path coq_path implicit =
 let add_vo_require opts d p export =
   { opts with pre = { opts.pre with vo_requires = (d, p, export) :: opts.pre.vo_requires }}
 
-let add_compat_require opts v =
-  match v with
-  | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
-  | Flags.V8_10 -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
-  | Flags.V8_11 -> add_vo_require opts "Coq.Compat.Coq811" None (Some false)
-  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq812" None (Some false)
-
 let add_load_vernacular opts verb s =
   { opts with pre = { opts.pre with load_vernacular_list = (CUnix.make_suffix s ".v",verb) :: opts.pre.load_vernacular_list }}
 
@@ -274,6 +267,18 @@ let get_native_name s =
       Nativelib.output_dir; Library.native_name_from_filename s]
   with _ -> ""
 
+let get_compat_file = function
+  | "8.12" -> "Coq.Compat.Coq812"
+  | "8.11" -> "Coq.Compat.Coq811"
+  | "8.10" -> "Coq.Compat.Coq810"
+  | "8.9" -> "Coq.Compat.Coq89"
+  | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+    CErrors.user_err ~hdr:"get_compat_file"
+      Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
+  | s ->
+    CErrors.user_err ~hdr:"get_compat_file"
+      Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
+
 let to_opt_key = Str.(split (regexp " +"))
 
 let parse_option_set opt =
@@ -379,9 +384,7 @@ let parse_args ~help ~init arglist : t * string list =
     |"-worker-id" -> set_worker_id opt (next ()); oval
 
     |"-compat" ->
-      let v = G_vernac.parse_compat_version (next ()) in
-      Flags.compat_version := v;
-      add_compat_require oval v
+      add_vo_require oval (get_compat_file (next ())) None (Some false)
 
     |"-exclude-dir" ->
       System.exclude_directory (next ()); oval
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5f088379ca..436648c163 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -62,18 +62,6 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
-let parse_compat_version = let open Flags in function
-  | "8.12" -> Current
-  | "8.11" -> V8_11
-  | "8.10" -> V8_10
-  | "8.9" -> V8_9
-  | ("8.8" | "8.7" | "8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
-    CErrors.user_err ~hdr:"get_compat_version"
-      Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
-  | s ->
-    CErrors.user_err ~hdr:"get_compat_version"
-      Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
-
 (* For now we just keep the top-level location of the whole
    vernacular, that is to say, including attributes and control flags;
    this is not very convenient for advanced clients tho, so in the
@@ -1192,7 +1180,7 @@ GRAMMAR EXTEND Gram
      | IDENT "Notation"; id = identref;
          idl = LIST0 ident; ":="; c = constr; b = only_parsing ->
            { VernacSyntacticDefinition
-             (id,(idl,c),b) }
+             (id,(idl,c),{ onlyparsing = b }) }
      | IDENT "Notation"; s = lstring; ":=";
          c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ];
@@ -1216,11 +1204,8 @@ GRAMMAR EXTEND Gram
   ] ]
   ;
   only_parsing:
-    [ [ "("; IDENT "only"; IDENT "parsing"; ")" ->
-         { Some Flags.Current }
-      | "("; IDENT "compat"; s = STRING; ")" ->
-         { Some (parse_compat_version s) }
-      | -> { None } ] ]
+    [ [ "("; IDENT "only"; IDENT "parsing"; ")" -> { true }
+      | -> { false } ] ]
   ;
   level:
     [ [ IDENT "level"; n = natural -> { NumLevel n }
@@ -1236,8 +1221,6 @@ GRAMMAR EXTEND Gram
       | IDENT "no"; IDENT "associativity" -> { SetAssoc Gramlib.Gramext.NonA }
       | IDENT "only"; IDENT "printing" -> { SetOnlyPrinting }
       | IDENT "only"; IDENT "parsing" -> { SetOnlyParsing }
-      | IDENT "compat"; s = STRING ->
-        { SetCompatVersion (parse_compat_version s) }
       | IDENT "format"; s1 = [s = STRING -> { CAst.make ~loc s } ];
                         s2 = OPT [s = STRING -> { CAst.make ~loc s } ] ->
           { begin match s1, s2 with
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index fd57901acd..e23522da9e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -805,7 +805,6 @@ type notation_modifier = {
   (* common to syn_data below *)
   only_parsing  : bool;
   only_printing : bool;
-  compat        : Flags.compat_version option;
   format        : lstring option;
   extra         : (string * string) list;
 }
@@ -818,7 +817,6 @@ let default = {
   subtyps       = [];
   only_parsing  = false;
   only_printing = false;
-  compat        = None;
   format        = None;
   extra         = [];
 }
@@ -877,8 +875,6 @@ let interp_modifiers modl = let open NotationMods in
         interp subtyps { acc with only_parsing = true; } l
     | SetOnlyPrinting :: l ->
         interp subtyps { acc with only_printing = true; } l
-    | SetCompatVersion v :: l ->
-        interp subtyps { acc with compat = Some v; } l
     | SetFormat ("text",s) :: l ->
         if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once.");
         interp subtyps { acc with format = Some s; } l
@@ -916,7 +912,6 @@ let check_binder_type recvars etyps =
 let not_a_syntax_modifier = function
 | SetOnlyParsing -> true
 | SetOnlyPrinting -> true
-| SetCompatVersion _ -> true
 | _ -> false
 
 let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
@@ -1213,32 +1208,12 @@ let check_locality_compatibility local custom i_typs =
                     strbrk " which is local."))
       (List.uniquize allcustoms)
 
-let warn_deprecated_compat =
-  CWarnings.create ~name:"deprecated-compat" ~category:"deprecated"
-    (fun () -> Pp.(str"The \"compat\" modifier is deprecated." ++ spc () ++
-                   str"Please use the \"deprecated\" attributed instead."))
-
-(* Returns the new deprecation and the onlyparsing status. This should be
-removed together with the compat syntax modifier. *)
-let merge_compat_deprecation compat deprecation =
-  match compat, deprecation with
-  | Some Flags.Current, _ -> deprecation, true
-  | Some _, Some _ ->
-    CErrors.user_err Pp.(str"The \"compat\" modifier cannot be used with the \"deprecated\" attribute."
-                        ++ spc () ++ str"Please use only the latter.")
-  | Some v, None ->
-    warn_deprecated_compat ();
-    Some (Deprecation.make ~since:(Flags.pr_version v) ()), true
-  | None, Some _ -> deprecation, true
-  | None, None -> deprecation, false
-
 let compute_syntax_data ~local deprecation df modifiers =
   let open SynData in
   let open NotationMods in
   let mods = interp_modifiers modifiers in
   let onlyprint = mods.only_printing in
   let onlyparse = mods.only_parsing in
-  let deprecation, _ = merge_compat_deprecation mods.compat deprecation in
   if onlyprint && onlyparse then user_err (str "A notation cannot be both 'only printing' and 'only parsing'.");
   let assoc = Option.append mods.assoc (Some Gramlib.Gramext.NonA) in
   let (recvars,mainvars,symbols) = analyze_notation_tokens ~onlyprint df in
@@ -1659,7 +1634,7 @@ let try_interp_name_alias = function
   | [], { CAst.v = CRef (ref,_) } -> intern_reference ref
   | _ -> raise Not_found
 
-let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
+let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
   let vars,reversibility,pat =
     try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
     with Not_found ->
@@ -1673,7 +1648,6 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) compat =
       let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
       List.map map vars, reversibility, pat
   in
-  let deprecation, onlyparsing = merge_compat_deprecation compat deprecation in
   let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
   Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
 
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 44e08c4819..e3e733a4b7 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntax_extension :
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
 val add_syntactic_definition : local:bool -> Deprecation.t option -> env ->
-  Id.t -> Id.t list * constr_expr -> Flags.compat_version option -> unit
+  Id.t -> Id.t list * constr_expr -> onlyparsing_flag -> unit
 
 (** Print the Camlp5 state of a grammar *)
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 1aa9a4e0f5..1742027076 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -412,7 +412,6 @@ let string_of_theorem_kind = let open Decls in function
     | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_simple_entry_type typ
     | SetOnlyPrinting -> keyword "only printing"
     | SetOnlyParsing -> keyword "only parsing"
-    | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
     | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s
     | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s
 
@@ -1059,16 +1058,12 @@ let string_of_definition_object_kind = let open Decls in function
         )
       | VernacHints (dbnames,h) ->
         return (pr_hints dbnames h (pr_constr env sigma) (pr_constr_pattern_expr env sigma))
-      | VernacSyntacticDefinition (id,(ids,c),compat) ->
+      | VernacSyntacticDefinition (id,(ids,c),{onlyparsing}) ->
         return (
           hov 2
             (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 Flags.Current -> [SetOnlyParsing]
-                | Some v -> [SetCompatVersion v]))
+               pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
         )
       | VernacArguments (q, args, more_implicits, mods) ->
         return (
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bb55cd5114..1bf34f2922 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1206,10 +1206,10 @@ let vernac_hints ~atts dbnames h =
   let local = enforce_module_locality local in
   Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h)
 
-let vernac_syntactic_definition ~atts lid x compat =
+let vernac_syntactic_definition ~atts lid x only_parsing =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
   Dumpglob.dump_definition lid false "syndef";
-  Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat
+  Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x only_parsing
 
 let default_env () = {
   Notation_term.ninterp_var_type = Id.Map.empty;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index bec6a0d2bb..32ff8b8fb2 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -105,7 +105,7 @@ 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 = Declarations.recursivity_kind
-type onlyparsing_flag = Flags.compat_version option
+type onlyparsing_flag = { onlyparsing : bool }
  (* 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 *)
@@ -185,7 +185,6 @@ type syntax_modifier =
   | SetEntryType of string * Extend.simple_constr_prod_entry_key
   | SetOnlyParsing
   | SetOnlyPrinting
-  | SetCompatVersion of Flags.compat_version
   | SetFormat of string * lstring
 
 type proof_end =