Merge PR #8637: Update -compat to support -compat 8.10

Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares

14 files changed, 237 insertions, 76 deletions

diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index b1c111685b..d05b6c8eef 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -4,37 +4,20 @@
 
 - [ ] Create a new issue to track the release process where you can copy-paste
   the present checklist.
-- [ ] Change the version name to the next major version and the magic numbers
-  (see [#7008](https://github.com/coq/coq/pull/7008/files)).
-- [ ] Update the compatibility infrastructure, which consists of doing
-      the following steps.  Note that all but the final step can be
-      performed automatically by
-      [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so
-      long as you have already updated `coq_version` in
-      [`configure.ml`](/configure.ml).
-  + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header
-        from [`dev/header.ml`](/dev/header.ml)
-  + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of
-        `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X.
-  + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions
-        prior to X.X.
-  + [ ] Update
-        [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template)
-        with the deleted/added files.
-  + [ ] Remove any notations in the standard library which have `compat "W.W"`.
-  + [ ] 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 files
-        [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
-        [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
-        and
-        [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v)
-        by bumping all version numbers by 1.
-  + [ ] Decide what to do about all test-suite files which mention `-compat
-        W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only
-        keep compatibility against the two previous versions)
+- [ ] Change the version name to the next major version and the magic
+  numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)).
+
+  Additionally, in the same commit, update the compatibility
+  infrastructure, which consists of invoking
+  [`dev/tools/update-compat.py`](../tools/update-compat.py) with the
+  `--master` flag.
+
+  Note that the `update-compat.py` script must be run twice: once
+  *immediately after* branching with the `--master` flag (which sets
+  up Coq to support four `-compat` flag arguments), *in the same
+  commit* as the one that updates `coq_version` in
+  [`configure.ml`](../../configure.ml), and once again later on before
+  the next branch point with the `--release` flag (see next section).
 - [ ] Put the corresponding alpha tag using `git tag -s`.
   The `VX.X+alpha` tag marks the first commit to be in `master` and not in the
   branch of the previous version.
@@ -43,6 +26,19 @@
   release date) and put this information in the milestone (using the
   description and due date fields).
 
+## Anytime after the previous version is branched off master ##
+
+- [ ] Update the compatibility infrastructure to the next release,
+  which consists of invoking
+  [`dev/tools/update-compat.py`](../tools/update-compat.py) with the
+  `--release` flag; this sets up Coq to support three `-compat` flag
+  arguments.  To ensure that CI passes, you will have to decide what
+  to do about all test-suite files which mention `-compat U.U` or
+  `Coq.Comapt.CoqUU` (which is no longer valid, since we only keep
+  compatibility against the two previous versions on releases), and
+  you may have to prepare overlays for projects using the
+  compatibility flags.
+
 ## About one month before the beta ##
 
 - [ ] Create the `X.X.0` milestone and set its due date.
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index 14094553a2..bde00a2f0d 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -1,6 +1,60 @@
 #!/usr/bin/env python
 from __future__ import with_statement
-import os, re, sys
+import os, re, sys, subprocess
+
+# When passed `--release`, this script sets up Coq to support three
+# `-compat` flag arguments.  If executed manually, this would consist
+# of doing the following steps:
+#
+# - Delete the file `theories/Compat/CoqUU.v`, where U.U is four
+#   versions prior to the new version X.X.  After this, there
+#   should be exactly three `theories/Compat/CoqNN.v` files.
+# - Update
+#   [`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).
+#
+# - Remove the file
+#   [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v).
+# - Update
+#   [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh)
+#   to ensure that it passes `--release` to the `update-compat.py`
+#   script.
+
+# When passed the `--master` flag, this script sets up Coq to support
+# four `-compat` flag arguments.  If executed manually, this would
+# consist of doing the following steps:
+#
+# - Add a file `theories/Compat/CoqXX.v` which contains just the header
+#   from [`dev/header.ml`](/dev/header.ml)
+# - Add the line `Require Export Coq.Compat.CoqXX.` at the top of
+#   `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X.
+# - 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 files
+#   [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v),
+#   [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v),
+#   and
+#   [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v)
+#   by bumping all version numbers by 1.  Re-create the file
+#   [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v)
+#   with its version numbers also bumped by 1 (file should have
+#   been removed before branching; see above).
+# - Update
+#   [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh)
+#   to ensure that it passes `--master` to the `update-compat.py`
+#   script.
+
+
 
 # Obtain the absolute path of the script being run.  By assuming that
 # the script lives in dev/tools/, and basing all calls on the path of
@@ -11,6 +65,8 @@ ROOT_PATH = os.path.realpath(os.path.join(SCRIPT_PATH, '..', '..'))
 CONFIGURE_PATH = os.path.join(ROOT_PATH, 'configure.ml')
 HEADER_PATH = os.path.join(ROOT_PATH, 'dev', 'header.ml')
 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')
@@ -18,6 +74,7 @@ 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')
 BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
+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)
                          for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
 TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current')
@@ -30,6 +87,29 @@ def get_header():
 
 HEADER = get_header()
 
+def break_or_continue():
+    msg = 'Press ENTER to continue, or Ctrl+C to break...'
+    try:
+        raw_input(msg)
+    except NameError: # we must be running python3
+        input(msg)
+
+def maybe_git_add(local_path, suggest_add=True, **args):
+    if args['git_add']:
+        print("Running 'git add %s'..." % local_path)
+        retc = subprocess.call(['git', 'add', local_path], cwd=ROOT_PATH)
+        if retc is not None and retc != 0:
+            print('!!! Process returned code %d' % retc)
+    elif suggest_add:
+        print(r"!!! Don't forget to 'git add %s'!" % local_path)
+
+def maybe_git_rm(local_path, **args):
+    if args['git_add']:
+        print("Running 'git rm %s'..." % local_path)
+        retc = subprocess.call(['git', 'rm', local_path], cwd=ROOT_PATH)
+        if retc is not None and retc != 0:
+            print('!!! Process returned code %d' % retc)
+
 def get_version(cur_version=None):
     if cur_version is not None: return cur_version
     with open(CONFIGURE_PATH, 'r') as f:
@@ -72,11 +152,47 @@ def get_known_versions():
 def get_new_versions(known_versions, **args):
     if args['cur_version'] in known_versions:
         assert(known_versions[-1] == args['cur_version'])
-        assert(len(known_versions) == args['number_of_compat_versions'])
-        return known_versions
+        known_versions = known_versions[:-1]
     assert(len(known_versions) >= args['number_of_old_versions'])
     return tuple(list(known_versions[-args['number_of_old_versions']:]) + [args['cur_version']])
 
+def print_diff(olds, news, numch=30):
+    for ch in range(min(len(olds), len(news))):
+        if olds[ch] != news[ch]:
+            print('Character %d differs:\nOld: %s\nNew: %s' % (ch, repr(olds[ch:][:numch]), repr(news[ch:][numch])))
+            return
+    ch = min(len(olds), len(news))
+    assert(len(olds) != len(news))
+    print('Strings are different lengths:\nOld tail: %s\nNew tail: %s' % (repr(olds[ch:]), repr(news[ch:])))
+
+def update_shebang_to_match(contents, new_contents, path):
+    contents_lines = contents.split('\n')
+    new_contents_lines = new_contents.split('\n')
+    if not (contents_lines[0].startswith('#!/') and contents_lines[0].endswith('bash')):
+        raise Exception('Unrecognized #! line in existing %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(contents_lines[0])))
+    if not (new_contents_lines[0].startswith('#!/') and new_contents_lines[0].endswith('bash')):
+        raise Exception('Unrecognized #! line in new %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(new_contents_lines[0])))
+    new_contents_lines[0] = contents_lines[0]
+    return '\n'.join(new_contents_lines)
+
+def update_if_changed(contents, new_contents, path, exn_string='%s changed!', suggest_add=False, pass_through_shebang=False, assert_unchanged=False, **args):
+    if contents is not None and pass_through_shebang:
+        new_contents = update_shebang_to_match(contents, new_contents, path)
+    if contents is None or contents != new_contents:
+        if not assert_unchanged:
+            print('Updating %s...' % os.path.relpath(path, ROOT_PATH))
+            with open(path, 'w') as f:
+                f.write(new_contents)
+            maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args)
+        else:
+            if contents is not None:
+                print('Unexpected change:\nOld contents:\n%s\n\nNew contents:\n%s\n' % (contents, new_contents))
+                print_diff(contents, new_contents)
+            raise Exception(exn_string % os.path.relpath(path, ROOT_PATH))
+
+def update_file(new_contents, path, **args):
+    update_if_changed(None, new_contents, path, **args)
+
 def update_compat_files(old_versions, new_versions, assert_unchanged=False, **args):
     for v in old_versions:
         if v not in new_versions:
@@ -85,6 +201,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
                 print('Removing %s...' % compat_file)
                 compat_path = os.path.join(ROOT_PATH, compat_file)
                 os.rename(compat_path, compat_path + '.bak')
+                maybe_git_rm(compat_file, **args)
             else:
                 raise Exception('%s exists!' % compat_file)
     for v, next_v in zip(new_versions, list(new_versions[1:]) + [None]):
@@ -95,12 +212,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
             contents = HEADER + (EXTRA_HEADER % v)
             if next_v is not None:
                 contents += '\nRequire Export Coq.Compat.%s.\n' % version_name_to_compat_name(next_v, ext='')
-            if not assert_unchanged:
-                with open(compat_path, 'w') as f:
-                    f.write(contents)
-                print(r"Don't forget to 'git add %s'!" % compat_file)
-            else:
-                raise Exception('%s does not exist!' % compat_file)
+            update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args)
         else:
             # print('Checking %s...' % compat_file)
             with open(compat_path, 'r') as f:
@@ -116,12 +228,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar
                     if not contents.startswith(header + '\n'):
                         contents = contents.replace(header, header + '\n')
                     contents = contents.replace(header, '%s\n%s' % (header, line))
-                    if not assert_unchanged:
-                        print('Updating %s...' % compat_file)
-                        with open(compat_path, 'w') as f:
-                            f.write(contents)
-                    else:
-                        raise Exception('Compat file %s is missing line %s' % (compat_file, 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'])
@@ -173,11 +280,18 @@ def update_add_compat_require(new_versions, contents, relpath):
     return new_contents
 
 def update_parse_compat_version(new_versions, contents, relpath, **args):
-    line_count = args['number_of_compat_versions']+2 # 1 for the first line, 1 for the invalid flags
+    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'
-    old_function_lines = contents[contents.index(first_line):].split('\n')[:line_count]
-    if re.match(r'^  \| \([0-9 "\.\|]*\) as s ->$', old_function_lines[-1]) is None:
-        raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions' % (line_count, relpath))
+    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:
+            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)))
+    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]
@@ -197,15 +311,6 @@ def check_no_old_versions(old_versions, new_versions, contents, relpath):
             if V in contents:
                 raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath))
 
-def update_if_changed(contents, new_contents, path, assert_unchanged=False, **args):
-    if contents != new_contents:
-        if not assert_unchanged:
-            print('Updating %s...' % os.path.relpath(path, ROOT_PATH))
-            with open(path, 'w') as f:
-                f.write(new_contents)
-        else:
-            raise Exception('%s changed!' % os.path.relpath(path, ROOT_PATH))
-
 def update_flags_mli(old_versions, new_versions, **args):
     with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read()
     new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH))
@@ -242,17 +347,20 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
     assert(len(new_versions) == len(test_suite_paths))
     assert(len(new_versions) == len(test_suite_descriptions))
     for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)):
-        if not os.path.exists(path):
-            raise Exception('Could not find existing file %s' % os.path.relpath(path, ROOT_PATH))
+        contents = None
+        suggest_add = False
+        if os.path.exists(path):
+            with open(path, 'r') as f: contents = f.read()
+        else:
+            suggest_add = True
         if '%s' in descr: descr = descr % v
-        with open(path, 'r') as f: contents = f.read()
         lines = ['(* -*- coq-prog-args: ("-compat" "%s") -*- *)' % v,
                  '(** Check that the %s compatibility flag actually requires the relevant modules. *)' % descr]
         for imp_v in reversed(new_versions[i:]):
             lines.append('Import Coq.Compat.%s.' % version_name_to_compat_name(imp_v, ext=''))
         lines.append('')
         new_contents = '\n'.join(lines)
-        update_if_changed(contents, new_contents, path, **args)
+        update_if_changed(contents, new_contents, path, suggest_add=suggest_add, **args)
 
 def update_doc_index(new_versions, **args):
     with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
@@ -264,6 +372,20 @@ def update_doc_index(new_versions, **args):
     new_contents = new_contents.replace(firstline, '\n'.join([firstline] + extra_lines))
     update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args)
 
+def update_test_suite_run(**args):
+    with open(TEST_SUITE_RUN_PATH, 'r') as f: contents = f.read()
+    new_contents = r'''#!/usr/bin/env bash
+
+# allow running this script from any directory by basing things on where the script lives
+SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
+
+# we assume that the script lives in test-suite/tools/update-compat/,
+# and that update-compat.py lives in dev/tools/
+cd "${SCRIPT_DIR}/../../.."
+dev/tools/update-compat.py --assert-unchanged %s || exit $?
+''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip()
+    update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args)
+
 def update_bug_4789(new_versions, **args):
     # we always update this compat notation to oldest
     # currently-supported compat version, which should never be the
@@ -305,11 +427,26 @@ def parse_args(argv):
     args = {
         'assert_unchanged': False,
         'cur_version': None,
-        'number_of_old_versions': DEFAULT_NUMBER_OF_OLD_VERSIONS
+        'number_of_old_versions': None,
+        'master': False,
+        'release': False,
+        'git_add': False,
     }
+    if '--master' not in argv and '--release' not in argv:
+        print(r'''WARNING: You should pass either --release (sometime before branching)
+  or --master (right after branching and updating the version number in version.ml)''')
+        if '--assert-unchanged' not in args: break_or_continue()
     for arg in argv[1:]:
         if arg == '--assert-unchanged':
             args['assert_unchanged'] = True
+        elif arg == '--git-add':
+            args['git_add'] = True
+        elif arg == '--master':
+            args['master'] = True
+            if args['number_of_old_versions'] is None: args['number_of_old_versions'] = MASTER_NUMBER_OF_OLD_VERSIONS
+        elif arg == '--release':
+            args['release'] = True
+            if args['number_of_old_versions'] is None: args['number_of_old_versions'] = RELEASE_NUMBER_OF_OLD_VERSIONS
         elif arg.startswith('--cur-version='):
             args['cur_version'] = arg[len('--cur-version='):]
             assert(len(args['cur_version'].split('.')) == 2)
@@ -317,10 +454,11 @@ def parse_args(argv):
         elif arg.startswith('--number-of-old-versions='):
             args['number_of_old_versions'] = int(arg[len('--number-of-old-versions='):])
         else:
-            print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN]' % argv[0])
+            print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN] [--git-add]' % argv[0])
             print('')
             print('ERROR: Unrecognized argument: %s' % arg)
             sys.exit(1)
+    if args['number_of_old_versions'] is None: args['number_of_old_versions'] = DEFAULT_NUMBER_OF_OLD_VERSIONS
     return args
 
 if __name__ == '__main__':
@@ -335,6 +473,7 @@ if __name__ == '__main__':
     update_compat_files(known_versions, new_versions, **args)
     update_flags(known_versions, new_versions, **args)
     update_test_suite(new_versions, **args)
+    update_test_suite_run(**args)
     update_doc_index(new_versions, **args)
     update_bug_4789(new_versions, **args)
     update_compat_notations(known_versions, new_versions, **args)
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 51f94d7e5a..c33df52038 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -618,5 +618,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq87.v
     theories/Compat/Coq88.v
     theories/Compat/Coq89.v
+    theories/Compat/Coq810.v
   </dd>
 </dl>
diff --git a/lib/flags.ml b/lib/flags.ml
index ae4d337ded..55bfa3cbde 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -66,7 +66,7 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_7 | V8_8 | Current
+type compat_version = V8_7 | V8_8 | V8_9 | Current
 
 let compat_version = ref Current
 
@@ -77,6 +77,9 @@ let version_compare v1 v2 = match v1, v2 with
   | V8_8, V8_8 -> 0
   | V8_8, _ -> -1
   | _, V8_8 -> 1
+  | V8_9, V8_9 -> 0
+  | V8_9, _ -> -1
+  | _, V8_9 -> 1
   | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
@@ -85,6 +88,7 @@ let version_less_or_equal v = not (version_strictly_greater v)
 let pr_version = function
   | V8_7 -> "8.7"
   | V8_8 -> "8.8"
+  | V8_9 -> "8.9"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index d883cf1e30..7336b9beaf 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -58,7 +58,7 @@ 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_7 | V8_8 | Current
+type compat_version = V8_7 | V8_8 | V8_9 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 5650dba236..81469d79c3 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq89.
+Import Coq.Compat.Coq810.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index 37d50ee67d..afeb57f9f2 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq810.
 Import Coq.Compat.Coq89.
 Import Coq.Compat.Coq88.
-Import Coq.Compat.Coq87.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..1f62635f50
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq89.
+Import Coq.Compat.Coq88.
+Import Coq.Compat.Coq87.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 9981388381..c8f75915c8 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq810.
 Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 02a2348450..61273c4f37 100755
--- a/test-suite/tools/update-compat/run.sh
+++ b/test-suite/tools/update-compat/run.sh
@@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
 # we assume that the script lives in test-suite/tools/update-compat/,
 # and that update-compat.py lives in dev/tools/
 cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged --cur-version=8.9 || exit $?
+dev/tools/update-compat.py --assert-unchanged --master || exit $?
diff --git a/theories/Compat/Coq810.v b/theories/Compat/Coq810.v
new file mode 100644
index 0000000000..f10201661e
--- /dev/null
+++ b/theories/Compat/Coq810.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.10 *)
diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v
index decb5c7519..05d63d9a47 100644
--- a/theories/Compat/Coq89.v
+++ b/theories/Compat/Coq89.v
@@ -11,5 +11,7 @@
 (** Compatibility file for making Coq act similar to Coq v8.9 *)
 Local Set Warnings "-deprecated".
 
+Require Export Coq.Compat.Coq810.
+
 Unset Private Polymorphic Universes.
 Set Refine Instance Mode.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 0a32879764..eaa050bdce 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -165,7 +165,8 @@ let add_compat_require opts v =
   match v with
   | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
   | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
-  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
+  | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
+  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false)
 
 let set_batch_mode opts =
   (* XXX: This should be in the argument record *)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3bc4aecdb1..79adefdcf7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -61,7 +61,8 @@ let make_bullet s =
   | _ -> assert false
 
 let parse_compat_version = let open Flags in function
-  | "8.9" -> Current
+  | "8.10" -> Current
+  | "8.9" -> V8_9
   | "8.8" -> V8_8
   | "8.7" -> V8_7
   | ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->