Merge PR #8634: (For v8.9 and master) Remove -compat 8.6 and document the compat updates to do as part of a release.

49 files changed, 1064 insertions, 1179 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 1c8ba5f53f..51fc2b035c 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -348,3 +348,7 @@
 
 /dev/tools/check-owners*.sh @SkySkimmer
 # Secondary maintainer @maximedenes
+
+/dev/tools/update-compat.py @JasonGross
+/test-suite/tools/update-compat/ @JasonGross
+# Secondary maintainer @Zimmi48
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 1821a181f1..b33a1cbd73 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -6,6 +6,35 @@
   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)
 - [ ] 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.
@@ -57,7 +86,6 @@
 ## Before the beta release date ##
 
 - [ ] Ensure the Credits chapter has been updated.
-- [ ] Ensure an empty `CompatXX.v` file has been created.
 - [ ] Ensure that an appropriate version of the plugins we will distribute with
   Coq has been tagged.
 - [ ] Have some people test the recently auto-generated Windows and MacOS
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
new file mode 100755
index 0000000000..7c8b9f025c
--- /dev/null
+++ b/dev/tools/update-compat.py
@@ -0,0 +1,341 @@
+#!/usr/bin/env python
+from __future__ import with_statement
+import os, re, sys
+
+# 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
+# the script, rather than the current working directory, we can be
+# robust to users who choose to run the script from any location.
+SCRIPT_PATH = os.path.dirname(os.path.realpath(__file__))
+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
+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')
+BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', '4798.v')
+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')
+# sanity check that we are where we think we are
+assert(os.path.normpath(os.path.realpath(SCRIPT_PATH)) == os.path.normpath(os.path.realpath(os.path.join(ROOT_PATH, 'dev', 'tools'))))
+assert(os.path.exists(CONFIGURE_PATH))
+
+def get_header():
+    with open(HEADER_PATH, 'r') as f: return f.read()
+
+HEADER = get_header()
+
+def get_version(cur_version=None):
+    if cur_version is not None: return cur_version
+    with open(CONFIGURE_PATH, 'r') as f:
+        for line in f.readlines():
+            found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line)
+            if len(found) > 0:
+                return found[0]
+    raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH))
+
+def compat_name_to_version_name(compat_file_name):
+    assert(compat_file_name.startswith('Coq') and compat_file_name.endswith('.v'))
+    v = compat_file_name[len('Coq'):][:-len('.v')]
+    assert(len(v) == 2 or (len(v) >= 2 and v[0] in ('8', '9'))) # we'll have to change this scheme when we hit Coq 10.*
+    return '%s.%s' % (v[0], v[1:])
+
+def version_name_to_compat_name(v, ext='.v'):
+    return 'Coq%s%s%s' % tuple(v.split('.') + [ext])
+
+# returns (lines of compat files, lines of not compat files
+def get_doc_index_lines():
+    with open(DOC_INDEX_PATH, 'r') as f:
+        lines = f.readlines()
+    return (tuple(line for line in lines if 'theories/Compat/Coq' in line),
+            tuple(line for line in lines if 'theories/Compat/Coq' not in line))
+
+COMPAT_INDEX_LINES, DOC_INDEX_LINES = get_doc_index_lines()
+
+def version_to_int_pair(v):
+    return tuple(map(int, v.split('.')))
+
+def get_known_versions():
+    # We could either get the files from the doc index, or from the
+    # directory list.  We assume that the doc index is more
+    # representative.  If we wanted to use the directory list, we
+    # would do:
+    # compat_files = os.listdir(os.path.join(ROOT_PATH, 'theories', 'Compat'))
+    compat_files = re.findall(r'Coq[^\.]+\.v', '\n'.join(COMPAT_INDEX_LINES))
+    return tuple(sorted((compat_name_to_version_name(i) for i in compat_files if i.startswith('Coq') and i.endswith('.v')), key=version_to_int_pair))
+
+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
+    assert(len(known_versions) >= args['number_of_old_versions'])
+    return tuple(list(known_versions[-args['number_of_old_versions']:]) + [args['cur_version']])
+
+def update_compat_files(old_versions, new_versions, assert_unchanged=False, **args):
+    for v in old_versions:
+        if v not in new_versions:
+            compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
+            if not assert_unchanged:
+                print('Removing %s...' % compat_file)
+                compat_path = os.path.join(ROOT_PATH, compat_file)
+                os.rename(compat_path, compat_path + '.bak')
+            else:
+                raise Exception('%s exists!' % compat_file)
+    for v, next_v in zip(new_versions, list(new_versions[1:]) + [None]):
+        compat_file = os.path.join('theories', 'Compat', version_name_to_compat_name(v))
+        compat_path = os.path.join(ROOT_PATH, compat_file)
+        if not os.path.exists(compat_path):
+            print('Creating %s...' % compat_file)
+            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)
+        else:
+            # print('Checking %s...' % compat_file)
+            with open(compat_path, 'r') as f:
+                contents = f.read()
+            header = HEADER + (EXTRA_HEADER % v)
+            if not contents.startswith(HEADER):
+                raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH)))
+            if not contents.startswith(header):
+                raise Exception("Invalid header in %s; missing line %s" % (compat_file, EXTRA_HEADER.strip('\n') % v))
+            if next_v is not None:
+                line = 'Require Export Coq.Compat.%s.' % version_name_to_compat_name(next_v, ext='')
+                if ('\n%s\n' % line) not in contents:
+                    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))
+
+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):
+    line_count = args['number_of_compat_versions']+2 # 1 for the first line, 1 for the invalid flags
+    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))
+    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']))):
+        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)
+    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_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))
+    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):
+    with open(FLAGS_ML_PATH, 'r') as f: contents = f.read()
+    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):
+    with open(COQARGS_ML_PATH, 'r') as f: contents = f.read()
+    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))
+    update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args)
+
+def update_g_vernac(old_versions, new_versions, **args):
+    with open(G_VERNAC_PATH, 'r') as f: contents = f.read()
+    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, **args):
+    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))
+        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)
+
+def update_doc_index(new_versions, **args):
+    with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
+    firstline = '    theories/Compat/AdmitAxiom.v'
+    new_contents = ''.join(DOC_INDEX_LINES)
+    if firstline not in new_contents:
+        raise Exception("Could not find line '%s' in %s" % (firstline, os.path.relpath(DOC_INDEX_PATH, ROOT_PATH)))
+    extra_lines = ['    theories/Compat/%s' % version_name_to_compat_name(v) for v in new_versions]
+    new_contents = new_contents.replace(firstline, '\n'.join([firstline] + extra_lines))
+    update_if_changed(contents, new_contents, DOC_INDEX_PATH, **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
+    # current version
+    with open(BUG_4798_PATH, 'r') as f: contents = f.read()
+    new_contents = r"""Check match 2 with 0 => 0 | S n => n end.
+Notation "|" := 1 (compat "%s").
+Check match 2 with 0 => 0 | S n => n end. (* fails *)
+""" % new_versions[0]
+    update_if_changed(contents, new_contents, BUG_4798_PATH, **args)
+
+def update_compat_notations_in(old_versions, new_versions, contents):
+    for v in old_versions:
+        if v not in new_versions:
+            reg = re.compile(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, flags=re.MULTILINE)
+            contents = re.sub(r'^[ \t]*(?:Notation|Infix)[^\n]*?compat "%s"[^\n]*?\n' % v, '', contents, flags=re.MULTILINE)
+    return contents
+
+def update_compat_notations(old_versions, new_versions, **args):
+    for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')):
+        for fname in files:
+            if not fname.endswith('.v'): continue
+            with open(os.path.join(root, fname), 'r') as f: contents = f.read()
+            new_contents = update_compat_notations_in(old_versions, new_versions, contents)
+            update_if_changed(contents, new_contents, os.path.join(root, fname), **args)
+
+def display_git_grep(old_versions, new_versions):
+    Vs = ['V%s_%s' % tuple(v.split('.')) for v in old_versions if v not in new_versions]
+    compat_vs = ['compat "%s"' % v for v in old_versions if v not in new_versions]
+    all_options = tuple(Vs + compat_vs)
+    options = (['"-compat" "%s"' % v for v in old_versions if v not in new_versions] +
+               [version_name_to_compat_name(v, ext='') for v in old_versions if v not in new_versions])
+    if len(options) > 0 or len(all_options) > 0:
+        print('To discover what files require manual updating, run:')
+        if len(options) > 0: print("git grep -- '%s' test-suite/" % r'\|'.join(options))
+        if len(all_options) > 0: print("git grep -- '%s'" % r'\|'.join(all_options))
+
+def parse_args(argv):
+    args = {
+        'assert_unchanged': False,
+        'cur_version': None,
+        'number_of_old_versions': DEFAULT_NUMBER_OF_OLD_VERSIONS
+    }
+    for arg in argv[1:]:
+        if arg == '--assert-unchanged':
+            args['assert_unchanged'] = True
+        elif arg.startswith('--cur-version='):
+            args['cur_version'] = arg[len('--cur-version='):]
+            assert(len(args['cur_version'].split('.')) == 2)
+            assert(all(map(str.isdigit, args['cur_version'].split('.'))))
+        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('')
+            print('ERROR: Unrecognized argument: %s' % arg)
+            sys.exit(1)
+    return args
+
+if __name__ == '__main__':
+    args = parse_args(sys.argv)
+    args['cur_version'] = get_version(args['cur_version'])
+    args['number_of_compat_versions'] = args['number_of_old_versions'] + 1
+    known_versions = get_known_versions()
+    new_versions = get_new_versions(known_versions, **args)
+    assert(len(TEST_SUITE_PATHS) >= args['number_of_compat_versions'])
+    args['test_suite_paths'] = tuple(TEST_SUITE_PATHS[-args['number_of_compat_versions']:])
+    args['test_suite_descriptions'] = tuple(TEST_SUITE_DESCRIPTIONS[-args['number_of_compat_versions']:])
+    update_compat_files(known_versions, new_versions, **args)
+    update_flags(known_versions, new_versions, **args)
+    update_test_suite(new_versions, **args)
+    update_doc_index(new_versions, **args)
+    update_bug_4789(new_versions, **args)
+    update_compat_notations(known_versions, new_versions, **args)
+    display_git_grep(known_versions, new_versions)
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0fa42cadad..4cbf75b715 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -600,8 +600,8 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq86.v
     theories/Compat/Coq87.v
     theories/Compat/Coq88.v
+    theories/Compat/Coq89.v
   </dd>
 </dl>
diff --git a/lib/flags.ml b/lib/flags.ml
index 4d6c36f55d..c8f19f2f11 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -66,25 +66,25 @@ 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_6 | V8_7 | Current
+type compat_version = V8_7 | V8_8 | Current
 
 let compat_version = ref Current
 
 let version_compare v1 v2 = match v1, v2 with
-  | V8_6, V8_6 -> 0
-  | V8_6, _ -> -1
-  | _, V8_6 -> 1
   | V8_7, V8_7 -> 0
   | V8_7, _ -> -1
   | _, V8_7 -> 1
+  | V8_8, V8_8 -> 0
+  | V8_8, _ -> -1
+  | _, V8_8 -> 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_6 -> "8.6"
   | V8_7 -> "8.7"
+  | V8_8 -> "8.8"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 398f22ab4f..3d9eafde75 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_6 | V8_7 | Current
+type compat_version = V8_7 | V8_8 | 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/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a40c0d2375..1b7f32bcae 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -790,9 +790,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
 	  | [], [] -> []
 	  | _ -> assert false
 	in aux 1 1 (List.rev nal) cs.cs_args, true in
-    let fsign = if Flags.version_strictly_greater Flags.V8_6
-                then Context.Rel.map (whd_betaiota !evdref) fsign
-                else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+    let fsign = Context.Rel.map (whd_betaiota !evdref) fsign in
     let fsign,env_f = push_rel_context !evdref fsign env in
     let obj ind p v f =
       if not record then
@@ -891,10 +889,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
 	let pi = lift n pred in (* liftn n 2 pred ? *)
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
         let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
-        let cs_args =
-          if Flags.version_strictly_greater Flags.V8_6
-          then Context.Rel.map (whd_betaiota !evdref) cs_args
-          else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+        let cs_args = Context.Rel.map (whd_betaiota !evdref) cs_args in
 	let csgn =
           List.map (set_name Anonymous) cs_args
         in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e223674579..4665486fc0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -193,10 +193,7 @@ let pose_all_metas_as_evars env evd t =
        | None ->
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
-        let ty =
-          if Flags.version_strictly_greater Flags.V8_6
-          then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
-          else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
+        let ty = nf_betaiota env evd ty in
         let src = Evd.evar_source_of_meta mv !evdref in
         let evd, ev = Evarutil.new_evar env !evdref ~src ty in
         evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd;
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 93ce519350..bde0bfc91f 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -102,7 +102,7 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
   coqdoc ssr
 
 # All subsystems
-SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-tests
+SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools unit-tests
 
 PREREQUISITELOG = prerequisite/admit.v.log			\
   prerequisite/make_local.v.log prerequisite/make_notation.v.log \
@@ -174,6 +174,7 @@ summary:
 	  $(call summary_dir, "Coqwc tests", coqwc); \
 	  $(call summary_dir, "Coq makefile", coq-makefile); \
 	  $(call summary_dir, "Coqdoc tests", coqdoc); \
+	  $(call summary_dir, "tools/ tests", tools); \
 	  $(call summary_dir, "Unit tests", unit-tests); \
 	  nb_success=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_success) | wc -l`; \
 	  nb_failure=`find . -name '*.log' -exec tail -n2 '{}' \; | grep -e $(log_failure) | wc -l`; \
@@ -652,3 +653,23 @@ $(addsuffix .log,$(wildcard coqdoc/*.v)): %.v.log: %.v %.html.out %.tex.out $(PR
 	    $(FAIL); \
 	  fi; \
 	} > "$@"
+
+# tools/
+
+tools: $(patsubst %/run.sh,%.log,$(wildcard tools/*/run.sh))
+
+tools/%.log : tools/%/run.sh
+	@echo "TEST      tools/$*"
+	$(HIDE)(\
+	  export COQBIN=$(BIN);\
+	  cd tools/$* && \
+	  bash run.sh 2>&1; \
+	if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	    $(FAIL); \
+	  fi; \
+	) > "$@"
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 6d73d58d4e..b9dd654057 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -73,7 +73,7 @@ Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
   end.
 Arguments LPTransfo : default implicits.
 
-Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := 
+Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f :=
   LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
 
 Section TTS.
@@ -121,8 +121,8 @@ Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predi
     Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2);
   simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 ->
     Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2);
-  simuPred: forall ext st, inv ext st -> 
-    (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p)) 
+  simuPred: forall ext st, inv ext st ->
+    (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p))
 }.
 
 Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)),
@@ -137,15 +137,15 @@ Qed.
 
 Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))):
   {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
-  fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
+  fun p => addIndex Ind _ (projT1 p) (tr (projT1 p) (projT2 p)).
 
 Arguments trProd : default implicits.
 Require Import Setoid.
 
 Theorem satTrProd:
-  forall State Ind Pred (tts: Ind -> TTS State) 
+  forall State Ind Pred (tts: Ind -> TTS State)
     (tr: forall i, (Pred  i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}),
-  lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p))
+  lpSat (Satisfy _ (tts (projT1 p))) st (tr (projT1 p) (projT2 p))
   <->
   lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p).
 Proof.
@@ -154,11 +154,11 @@ Proof.
                       (fun i => Satisfy _ (tts i))); tauto.
 Qed.
 
-Theorem simuProd: 
-  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+Theorem simuProd:
+  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC)
     (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
     (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
-     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> 
+     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) ->
        simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
                   (trProd Pred tta tra) (trProd Pred ttc trc).
 Proof.
@@ -171,11 +171,11 @@ Proof.
   eapply simuDelay; eauto.
   eapply simuNext; eauto.
   split; simpl; intros.
-  generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  generalize (proj1 (simuPred _ _ _ _ _ (X (projT1 p)) ext st (H (projT1 p)) (projT2 p))); simpl; intro.
   rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1.
   rewrite (satTrProd StateC Ind Pred ttc trc); apply H0.
 
-  generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  generalize (proj2 (simuPred _ _ _ _ _ (X (projT1 p)) ext st (H (projT1 p)) (projT2 p))); simpl; intro.
   rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1.
   rewrite (satTrProd StateA Ind Pred tta tra); apply H0.
 Qed.
@@ -189,11 +189,11 @@ Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra:
   simuRL: simu StateC StateA m2 Pred c a trc tra
 }.
 
-Theorem simu_equivProd: 
-  forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+Theorem simu_equivProd:
+  forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC)
     (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
     (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
-     (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) -> 
+     (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) ->
        simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
                   (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc).
 Proof.
@@ -237,7 +237,7 @@ Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & M
 
 (* product with shared state *)
 
-Definition PLanguage (L: RTLanguage): RTLanguage := 
+Definition PLanguage (L: RTLanguage): RTLanguage :=
   mkRTLanguage
     (PSyntax L)
     (pState L)
@@ -246,7 +246,7 @@ Definition PLanguage (L: RTLanguage): RTLanguage :=
         eq_refl => Semantic L (pComponents L mdl i)
        end))
     (pPredicate L)
-    (fun mdl => trProd _ _ _ _ 
+    (fun mdl => trProd _ _ _ _
       (fun i pi => match pIsShared L mdl i as e in (_ = y) return
                      (LP (Predicate y
                                match e in (_ = y0) return (TTS y0) with
@@ -259,22 +259,22 @@ Definition PLanguage (L: RTLanguage): RTLanguage :=
 Inductive Empty: Type :=.
 
 Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf {
-sameState:  forall mdl i j, 
+sameState:  forall mdl i j,
   DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
   DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j));
-sameMState: forall mdl i j, 
+sameMState: forall mdl i j,
   mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl i)) =
   mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl j));
-sameM12: forall mdl i j, 
+sameM12: forall mdl i j,
   Tl1l2 _ _ tr (pComponents l1 mdl i) =
   match sym_eq (sameState mdl i j) in _=y return mapping _ y with
     eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with
       eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with
         eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j)
       end
-    end         
+    end
   end;
-sameM21: forall mdl i j, 
+sameM21: forall mdl i j,
   Tl2l1 l1 l2 tr (pComponents l1 mdl i) =
   match
     sym_eq (sameState mdl i j) in (_ = y)
@@ -301,7 +301,7 @@ end
 Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
   mkPSyntax l2 (pIndex l1 mdl)
     (pIsEmpty l1 mdl)
-    (match pIsEmpty l1 mdl return Type with 
+    (match pIsEmpty l1 mdl return Type with
          inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
         |inright h => pState l1 mdl
        end)
@@ -314,7 +314,7 @@ Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
          | inright _ => pState l1 mdl
          end)
       with
-         inleft j => sameState l1 l2 tr h mdl i j 
+         inleft j => sameState l1 l2 tr h mdl i j
       | inright h => match h i with end
         end).
 
@@ -388,12 +388,12 @@ match pIsEmpty l1 mdl with
       addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x
         (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x))
           (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p))
-| inright f => match f (projS1 pp) with end
+| inright f => match f (projT1 pp) with end
 end.
 
-Lemma simu_eqA: 
+Lemma simu_eqA:
   forall A1 A2 C m P sa sc tta ttc (h: A2=A1),
-  simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end) 
+  simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end)
   P (match h in (_=y) return TTS y with eq_refl => sa end)
   sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end)
   ttc ->
@@ -401,9 +401,9 @@ Lemma simu_eqA:
 admit.
 Qed.
 
-Lemma simu_eqC: 
+Lemma simu_eqC:
   forall A C1 C2 m P sa sc tta ttc (h: C2=C1),
-  simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end) 
+  simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end)
   P sa (match h in (_=y) return TTS y with eq_refl => sc end)
   tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end)
    ->
@@ -411,10 +411,10 @@ Lemma simu_eqC:
 admit.
 Qed.
 
-Lemma simu_eqA1: 
+Lemma simu_eqA1:
   forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
-  simu A1 C m 
-  P 
+  simu A1 C m
+  P
   (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc
   (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc
    ->
@@ -422,32 +422,32 @@ Lemma simu_eqA1:
 admit.
 Qed.
 
-Lemma simu_eqA2: 
+Lemma simu_eqA2:
   forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
   simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end)
-  P 
+  P
   sa sc tta ttc
    ->
   simu A2 C m P
-  (match h in (_=y) return TTS y with eq_refl => sa end) sc 
+  (match h in (_=y) return TTS y with eq_refl => sa end) sc
   (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end)
  ttc.
 admit.
 Qed.
 
-Lemma simu_eqC2: 
+Lemma simu_eqC2:
   forall A C1 C2 m P sa sc tta ttc (h: C1=C2),
   simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end)
-  P 
+  P
   sa sc tta ttc
    ->
   simu A C2 m P
-  sa (match h in (_=y) return TTS y with eq_refl => sc end) 
+  sa (match h in (_=y) return TTS y with eq_refl => sc end)
   tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end).
 admit.
 Qed.
 
-Lemma simu_eqM: 
+Lemma simu_eqM:
   forall A C m1 m2 P sa sc tta ttc (h: m1=m2),
   simu A C m1 P sa sc tta ttc
    ->
@@ -470,7 +470,7 @@ Lemma LPTransfo_addIndex:
         addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))
       (addIndex Ind Pred x p).
 Proof.
-  unfold addIndex; intros. 
+  unfold addIndex; intros.
   rewrite LPTransfo_trans.
   rewrite LPTransfo_trans.
   simpl.
@@ -491,7 +491,7 @@ Lemma LPTransfo_addIndex_tr:
         addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))))
       (addIndex Ind Pred x p).
 Proof.
-  unfold addIndex; simpl; intros. 
+  unfold addIndex; simpl; intros.
   rewrite LPTransfo_trans; simpl.
   rewrite <- LPTransfo_trans.
   f_equal.
@@ -505,19 +505,19 @@ Qed.
 Require Export Coq.Logic.FunctionalExtensionality.
 Print PLanguage.
 
-Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
+Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr):
 Transformation (PLanguage l1) (PLanguage l2) :=
   mkTransformation (PLanguage l1) (PLanguage l2)
     (PTransfoSyntax l1 l2 tr h)
     (Pmap12 l1 l2 tr h)
     (Pmap21 l1 l2 tr h)
     (PTpred l1 l2 tr h)
-    (fun mdl => simu_equivProd 
-      (pState l1 mdl) 
-      (pState l2 (PTransfoSyntax l1 l2 tr h mdl)) 
+    (fun mdl => simu_equivProd
+      (pState l1 mdl)
+      (pState l2 (PTransfoSyntax l1 l2 tr h mdl))
       (Pmap12 l1 l2 tr h mdl)
       (Pmap21 l1 l2 tr h mdl)
-      (pIndex l1 mdl) 
+      (pIndex l1 mdl)
       (fun i => MdlPredicate l1 (pComponents l1 mdl i))
       (compSemantic l1 mdl)
       (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl))
diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v
index 28f028ad89..80c348d207 100644
--- a/test-suite/bugs/closed/4306.v
+++ b/test-suite/bugs/closed/4306.v
@@ -1,13 +1,13 @@
 Require Import List.
 Require Import Arith.
-Require Import Recdef. 
+Require Import Recdef.
 Require Import Omega.
 
 Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
   match xys with
     | (nil, _) => snd xys
     | (_, nil) => fst xys
-    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+    | (x :: xs', y :: ys') => match Nat.compare x y with
                                 | Lt => x :: foo (xs', y :: ys')
                                 | Eq => x :: foo (xs', ys')
                                 | Gt => y :: foo (x :: xs', ys')
@@ -24,7 +24,7 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
   match (xs, ys) with
     | (nil, _) => ys
     | (_, nil) => xs
-    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+    | (x :: xs', y :: ys') => match Nat.compare x y with
                                 | Lt => x :: foo (xs', ys)
                                 | Eq => x :: foo (xs', ys')
                                 | Gt => y :: foo (xs, ys')
diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v
index 6f2bcb9685..41a1251ca5 100644
--- a/test-suite/bugs/closed/4798.v
+++ b/test-suite/bugs/closed/4798.v
@@ -1,3 +1,3 @@
 Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.6").
+Notation "|" := 1 (compat "8.7").
 Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 1307a8f26d..975b2ef7ff 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -85,8 +85,8 @@ bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
-Notation existS2 := existT2
-Expands to: Notation Coq.Init.Specif.existS2
+Notation sym_eq := eq_sym
+Expands to: Notation Coq.Init.Logic.sym_eq
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index a498db3e89..62aa80f8ab 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -26,8 +26,7 @@ About bar.
 Print bar.
 
 About Peano. (* Module *)
-Set Warnings "-deprecated".
-About existS2. (* Notation *)
+About sym_eq. (* Notation *)
 
 Arguments eq_refl {A} {x}, {A} x.
 Print eq_refl.
@@ -46,4 +45,3 @@ Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False.
   About g.                              (* search hypothesis *)
   About h.                              (* search hypothesis *)
 Abort.
-
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 06357cfc21..3c427237b4 100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
@@ -23,7 +23,7 @@ Require Export ZArithRing.
 Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
 
 Ltac Flip :=
-  apply Zgt_lt || apply Zlt_gt || apply Zle_ge || apply Zge_le; assumption.
+  apply Z.gt_lt || apply Z.lt_gt || apply Z.le_ge || apply Z.ge_le; assumption.
 
 Ltac Falsum :=
   try intro; apply False_ind;
@@ -37,12 +37,12 @@ Ltac Falsum :=
 Ltac Step_l a :=
   match goal with
   |  |- (?X1 < ?X2)%Z => replace X1 with a; [ idtac | try ring ]
-  end. 
+  end.
 
 Ltac Step_r a :=
   match goal with
   |  |- (?X1 < ?X2)%Z => replace X2 with a; [ idtac | try ring ]
-  end. 
+  end.
 
 Ltac CaseEq formula :=
   generalize (refl_equal formula); pattern formula at -1 in |- *;
@@ -53,7 +53,7 @@ Lemma pair_1 : forall (A B : Set) (H : A * B), H = pair (fst H) (snd H).
 Proof.
  intros.
  case H.
- intros. 
+ intros.
  simpl in |- *.
  reflexivity.
 Qed.
@@ -73,10 +73,10 @@ Proof.
 Qed.
 
 
-Section projection.   
+Section projection.
  Variable A : Set.
  Variable P : A -> Prop.
- 
+
  Definition projP1 (H : sig P) := let (x, h) := H in x.
  Definition projP2 (H : sig P) :=
    let (x, h) as H return (P (projP1 H)) := H in h.
@@ -131,11 +131,11 @@ Declare Right Step neq_stepr.
 
 
 Lemma not_O_S : forall n : nat, n <> 0 -> {p : nat | n = S p}.
-Proof. 
+Proof.
  intros [| np] Hn; [ exists 0; apply False_ind; apply Hn | exists np ];
-  reflexivity. 
+  reflexivity.
 Qed.
-  
+
 
 Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0.
 Proof.
@@ -156,12 +156,12 @@ Proof.
 Qed.
 
 Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0.
-Proof. 
+Proof.
  intros; omega.
 Qed.
 
 Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0.
-Proof. 
+Proof.
  intros; omega.
 Qed.
 
@@ -228,8 +228,8 @@ Proof.
  assumption.
  intro.
  right.
- apply Zle_lt_trans with (m := x).
- apply Zge_le.
+ apply Z.le_lt_trans with (m := x).
+ apply Z.ge_le.
  assumption.
  assumption.
 Qed.
@@ -268,7 +268,7 @@ Proof.
  left.
  assumption.
  intro H0.
- generalize (Zge_le _ _ H0).
+ generalize (Z.ge_le _ _ H0).
  intro.
  case (Z_le_lt_eq_dec _ _ H1).
  intro.
@@ -290,25 +290,25 @@ Proof.
  left.
  assumption.
  intro H.
- generalize (Zge_le _ _ H).
+ generalize (Z.ge_le _ _ H).
  intro H0.
  case (Z_le_lt_eq_dec y x H0).
  intro H1.
  left.
  right.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  intro.
  right.
  symmetry  in |- *.
  assumption.
 Qed.
- 
+
 
 Lemma Z_dec' : forall x y : Z, {(x < y)%Z} + {(y < x)%Z} + {x = y}.
 Proof.
  intros x y.
- case (Z_eq_dec x y); intro H;
+ case (Z.eq_dec x y); intro H;
   [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
 Qed.
 
@@ -321,7 +321,7 @@ Proof.
  assumption.
  intro.
  right.
- apply Zge_le.
+ apply Z.ge_le.
  assumption.
 Qed.
 
@@ -335,7 +335,7 @@ Lemma Z_lt_lt_S_eq_dec :
 Proof.
  intros.
  generalize (Zlt_le_succ _ _ H).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  apply Z_le_lt_eq_dec.
 Qed.
 
@@ -347,7 +347,7 @@ Proof.
  case (Z_lt_le_dec a c).
  intro z.
  right.
- intro. 
+ intro.
  elim H.
  intros.
  generalize z.
@@ -356,8 +356,8 @@ Proof.
  intro.
  case (Z_lt_le_dec b d).
  intro z0.
- right. 
- intro. 
+ right.
+ intro.
  elim H.
  intros.
  generalize z0.
@@ -367,7 +367,7 @@ Proof.
  left.
  split.
  assumption.
- assumption. 
+ assumption.
 Qed.
 
 (*###########################################################################*)
@@ -386,30 +386,30 @@ Qed.
 
 Lemma Zlt_minus : forall a b : Z, (b < a)%Z -> (0 < a - b)%Z.
 Proof.
- intros a b. 
+ intros a b.
  intros.
  apply Zplus_lt_reg_l with b.
- unfold Zminus in |- *. 
+ unfold Zminus in |- *.
  rewrite (Zplus_comm a).
- rewrite (Zplus_assoc b (- b)). 
+ rewrite (Zplus_assoc b (- b)).
  rewrite Zplus_opp_r.
- simpl in |- *. 
- rewrite <- Zplus_0_r_reverse. 
+ simpl in |- *.
+ rewrite <- Zplus_0_r_reverse.
  assumption.
 Qed.
 
 
 Lemma Zle_minus : forall a b : Z, (b <= a)%Z -> (0 <= a - b)%Z.
 Proof.
- intros a b. 
+ intros a b.
  intros.
  apply Zplus_le_reg_l with b.
- unfold Zminus in |- *. 
+ unfold Zminus in |- *.
  rewrite (Zplus_comm a).
- rewrite (Zplus_assoc b (- b)). 
+ rewrite (Zplus_assoc b (- b)).
  rewrite Zplus_opp_r.
- simpl in |- *. 
- rewrite <- Zplus_0_r_reverse. 
+ simpl in |- *.
+ rewrite <- Zplus_0_r_reverse.
  assumption.
 Qed.
 
@@ -417,7 +417,7 @@ Lemma Zlt_plus_plus :
  forall m n p q : Z, (m < n)%Z -> (p < q)%Z -> (m + p < n + q)%Z.
 Proof.
  intros.
- apply Zlt_trans with (m := (n + p)%Z).
+ apply Z.lt_trans with (m := (n + p)%Z).
  rewrite Zplus_comm.
  rewrite Zplus_comm with (n := n).
  apply Zplus_lt_compat_l.
@@ -459,11 +459,11 @@ Lemma Zge_gt_plus_plus :
 Proof.
  intros.
  case (Zle_lt_or_eq n m).
- apply Zge_le.
+ apply Z.ge_le.
  assumption.
  intro.
  apply Zgt_plus_plus.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  assumption.
  intro.
@@ -521,7 +521,7 @@ Qed.
 
 
 Lemma Zle_neg_opp : forall x : Z, (x <= 0)%Z -> (0 <= - x)%Z.
-Proof. 
+Proof.
  intros.
  apply Zplus_le_reg_l with x.
  rewrite Zplus_opp_r.
@@ -530,7 +530,7 @@ Proof.
 Qed.
 
 Lemma Zle_pos_opp : forall x : Z, (0 <= x)%Z -> (- x <= 0)%Z.
-Proof. 
+Proof.
  intros.
  apply Zplus_le_reg_l with x.
  rewrite Zplus_opp_r.
@@ -542,7 +542,7 @@ Qed.
 Lemma Zge_opp : forall x y : Z, (x <= y)%Z -> (- x >= - y)%Z.
 Proof.
  intros.
- apply Zle_ge.
+ apply Z.le_ge.
  apply Zplus_le_reg_l with (p := (x + y)%Z).
  ring_simplify (x + y + - y)%Z (x + y + - x)%Z.
  assumption.
@@ -584,8 +584,8 @@ Proof.
  ring_simplify (- a * x + a * x)%Z.
  replace (- a * x + a * y)%Z with ((y - x) * a)%Z.
  apply Zmult_gt_0_le_0_compat.
- apply Zlt_gt.
- assumption. 
+ apply Z.lt_gt.
+ assumption.
  unfold Zminus in |- *.
  apply Zle_left.
  assumption.
@@ -621,7 +621,7 @@ Proof.
  rewrite H0.
  reflexivity.
 Qed.
- 
+
 Lemma Zsimpl_mult_l :
  forall n m p : Z, n <> 0%Z -> (n * m)%Z = (n * p)%Z -> m = p.
 Proof.
@@ -642,14 +642,14 @@ Lemma Zlt_reg_mult_l :
 Proof.
  intros.
  case (Zcompare_Gt_spec x 0).
- unfold Zgt in H.
+ unfold Z.gt in H.
  assumption.
  intros.
- cut (x = Zpos x0). 
+ cut (x = Zpos x0).
  intro.
  rewrite H2.
- unfold Zlt in H0.
- unfold Zlt in |- *.
+ unfold Z.lt in H0.
+ unfold Z.lt in |- *.
  cut ((Zpos x0 * y ?= Zpos x0 * z)%Z = (y ?= z)%Z).
  intro.
  exact (trans_eq H3 H0).
@@ -672,10 +672,10 @@ Proof.
  intro.
  cut ((y ?= x)%Z = (- x ?= - y)%Z).
  intro.
- exact (trans_eq H0 H1). 
+ exact (trans_eq H0 H1).
  exact (Zcompare_opp y x).
  apply sym_eq.
- exact (Zlt_gt x y H).
+ exact (Z.lt_gt x y H).
 Qed.
 
 
@@ -698,22 +698,22 @@ Proof.
  intro.
  rewrite H6 in H4.
  assumption.
- exact (Zopp_involutive (x * z)).
- exact (Zopp_involutive (x * y)).
+ exact (Z.opp_involutive (x * z)).
+ exact (Z.opp_involutive (x * y)).
  cut ((- (- x * y))%Z = (- - (x * y))%Z).
  intro.
  rewrite H4 in H3.
- cut ((- (- x * z))%Z = (- - (x * z))%Z). 
+ cut ((- (- x * z))%Z = (- - (x * z))%Z).
  intro.
  rewrite H5 in H3.
  assumption.
  cut ((- x * z)%Z = (- (x * z))%Z).
  intro.
- exact (f_equal Zopp H5).
+ exact (f_equal Z.opp H5).
  exact (Zopp_mult_distr_l_reverse x z).
  cut ((- x * y)%Z = (- (x * y))%Z).
  intro.
- exact (f_equal Zopp H4).
+ exact (f_equal Z.opp H4).
  exact (Zopp_mult_distr_l_reverse x y).
  exact (Zlt_opp (- x * y) (- x * z) H2).
  exact (Zlt_reg_mult_l (- x) y z H1 H0).
@@ -735,14 +735,14 @@ Proof.
  assumption.
  exact (sym_eq H2).
  exact (Zorder.Zlt_not_eq y x H0).
- exact (Zgt_lt x y H).
+ exact (Z.gt_lt x y H).
 Qed.
 
 Lemma Zmult_resp_nonzero :
  forall x y : Z, x <> 0%Z -> y <> 0%Z -> (x * y)%Z <> 0%Z.
 Proof.
  intros x y Hx Hy Hxy.
- apply Hx. 
+ apply Hx.
  apply Zmult_integral_l with y; assumption.
 Qed.
 
@@ -769,12 +769,12 @@ Qed.
 
 Lemma not_Zle_lt : forall x y : Z, ~ (y <= x)%Z -> (x < y)%Z.
 Proof.
- intros; apply Zgt_lt; apply Znot_le_gt; assumption.
+ intros; apply Z.gt_lt; apply Znot_le_gt; assumption.
 Qed.
 
 Lemma not_Zlt : forall x y : Z, ~ (y < x)%Z -> (x <= y)%Z.
 Proof.
- intros x y H1 H2; apply H1; apply Zgt_lt; assumption.
+ intros x y H1 H2; apply H1; apply Z.gt_lt; assumption.
 Qed.
 
 
@@ -813,7 +813,7 @@ Proof.
  cut (x > 0)%Z.
  intro.
  exact (Zlt_reg_mult_l x y z H4 H2).
- exact (Zlt_gt 0 x H3).
+ exact (Z.lt_gt 0 x H3).
  intro.
  apply False_ind.
  cut (x * z < x * y)%Z.
@@ -849,7 +849,7 @@ Proof.
  cut (x > 0)%Z.
  intro.
  exact (Zlt_reg_mult_l x z y H4 H2).
- exact (Zlt_gt 0 x H3).
+ exact (Z.lt_gt 0 x H3).
 Qed.
 
 Lemma Zlt_mult_mult :
@@ -857,9 +857,9 @@ Lemma Zlt_mult_mult :
  (0 < a)%Z -> (0 < d)%Z -> (a < b)%Z -> (c < d)%Z -> (a * c < b * d)%Z.
 Proof.
  intros.
- apply Zlt_trans with (a * d)%Z.
+ apply Z.lt_trans with (a * d)%Z.
  apply Zlt_reg_mult_l.
- Flip. 
+ Flip.
  assumption.
  rewrite Zmult_comm.
  rewrite Zmult_comm with b d.
@@ -881,11 +881,11 @@ Proof.
  apply Zgt_not_eq.
  assumption.
  trivial.
- 
+
  intro.
  case (not_Zeq x y H1).
  trivial.
- 
+
  intro.
  apply False_ind.
  cut (a * y > a * x)%Z.
@@ -913,14 +913,14 @@ Proof.
  rewrite Zmult_opp_opp.
  rewrite Zmult_opp_opp.
  assumption.
- apply Zopp_involutive.
- apply Zopp_involutive.
- apply Zgt_lt.
+ apply Z.opp_involutive.
+ apply Z.opp_involutive.
+ apply Z.gt_lt.
  apply Zlt_opp.
- apply Zgt_lt.
+ apply Z.gt_lt.
  assumption.
  simpl in |- *.
- rewrite Zopp_involutive.
+ rewrite Z.opp_involutive.
  assumption.
 Qed.
 
@@ -944,7 +944,7 @@ Proof.
  constructor.
  replace (-1 * y)%Z with (- y)%Z.
  replace (-1 * x)%Z with (- x)%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  ring.
  ring.
@@ -959,13 +959,13 @@ Proof.
  trivial.
  intro.
  apply False_ind.
- apply (Zlt_irrefl (a * x)).
- apply Zle_lt_trans with (m := (a * y)%Z).
+ apply (Z.lt_irrefl (a * x)).
+ apply Z.le_lt_trans with (m := (a * y)%Z).
  assumption.
- apply Zgt_lt.
+ apply Z.gt_lt.
  apply Zlt_conv_mult_l.
  assumption.
- apply Zgt_lt.
+ apply Z.gt_lt.
  assumption.
 Qed.
 
@@ -973,17 +973,17 @@ Lemma Zlt_mult_cancel_l :
  forall x y z : Z, (0 < x)%Z -> (x * y < x * z)%Z -> (y < z)%Z.
 Proof.
  intros.
- apply Zgt_lt.
+ apply Z.gt_lt.
  apply Zgt_mult_reg_absorb_l with x.
- apply Zlt_gt.
- assumption. 
- apply Zlt_gt.
+ apply Z.lt_gt.
+ assumption.
+ apply Z.lt_gt.
  assumption.
 Qed.
- 
+
 
 Lemma Zmin_cancel_Zle : forall x y : Z, (- x <= - y)%Z -> (y <= x)%Z.
-Proof. 
+Proof.
  intros.
  apply Zmult_cancel_Zle with (a := (-1)%Z).
  constructor.
@@ -1004,18 +1004,18 @@ Proof.
  trivial.
  intro.
  apply False_ind.
- apply (Zlt_irrefl (a * y)).
- apply Zle_lt_trans with (m := (a * x)%Z).
+ apply (Z.lt_irrefl (a * y)).
+ apply Z.le_lt_trans with (m := (a * x)%Z).
  assumption.
  apply Zlt_reg_mult_l.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
- apply Zgt_lt.
+ apply Z.gt_lt.
  assumption.
 Qed.
 
 Lemma Zopp_Zle : forall x y : Z, (y <= x)%Z -> (- x <= - y)%Z.
-Proof. 
+Proof.
  intros.
  apply Zmult_cancel_Zle with (a := (-1)%Z).
  constructor.
@@ -1026,7 +1026,7 @@ Proof.
  clear x H; ring.
 Qed.
 
- 
+
 Lemma Zle_lt_eq_S : forall x y : Z, (x <= y)%Z -> (y < x + 1)%Z -> y = x.
 Proof.
  intros.
@@ -1035,8 +1035,8 @@ Proof.
  apply False_ind.
  generalize (Zlt_le_succ x y H1).
  intro.
- apply (Zlt_not_le y (x + 1) H0).  
- replace (x + 1)%Z with (Zsucc x).
+ apply (Zlt_not_le y (x + 1) H0).
+ replace (x + 1)%Z with (Z.succ x).
  assumption.
  reflexivity.
  intro H1.
@@ -1053,8 +1053,8 @@ Proof.
  apply False_ind.
  generalize (Zlt_le_succ x y H).
  intro.
- apply (Zlt_not_le y (x + 1) H1).  
- replace (x + 1)%Z with (Zsucc x).
+ apply (Zlt_not_le y (x + 1) H1).
+ replace (x + 1)%Z with (Z.succ x).
  assumption.
  reflexivity.
  trivial.
@@ -1067,9 +1067,9 @@ Proof.
  intros.
  case (Z_zerop c).
  intro.
- rewrite e.  
+ rewrite e.
  left.
- apply sym_not_eq. 
+ apply sym_not_eq.
  intro.
  apply H; repeat split; assumption.
  intro; right; assumption.
@@ -1085,21 +1085,21 @@ Proof.
                   [ apply False_ind; apply H; repeat split | right; right ]
                | right; left ]
             | left ]; assumption.
-Qed. 
+Qed.
 
 Lemma mediant_1 :
  forall m n m' n' : Z, (m' * n < m * n')%Z -> ((m + m') * n < m * (n + n'))%Z.
 Proof.
- intros. 
- rewrite Zmult_plus_distr_r. 
+ intros.
+ rewrite Zmult_plus_distr_r.
  rewrite Zmult_plus_distr_l.
  apply Zplus_lt_compat_l.
  assumption.
 Qed.
- 
+
 Lemma mediant_2 :
  forall m n m' n' : Z,
- (m' * n < m * n')%Z -> (m' * (n + n') < (m + m') * n')%Z. 
+ (m' * n < m * n')%Z -> (m' * (n + n') < (m + m') * n')%Z.
 Proof.
  intros.
  rewrite Zmult_plus_distr_l.
@@ -1121,7 +1121,7 @@ Proof.
  assumption.
  assumption.
  ring.
-Qed. 
+Qed.
 
 Lemma fraction_lt_trans :
  forall a b c d e f : Z,
@@ -1130,21 +1130,21 @@ Lemma fraction_lt_trans :
  (0 < f)%Z -> (a * d < c * b)%Z -> (c * f < e * d)%Z -> (a * f < e * b)%Z.
 Proof.
  intros.
- apply Zgt_lt.
+ apply Z.gt_lt.
  apply Zgt_mult_reg_absorb_l with d.
  Flip.
  apply Zgt_trans with (c * b * f)%Z.
  replace (d * (e * b))%Z with (b * (e * d))%Z.
  replace (c * b * f)%Z with (b * (c * f))%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  apply Zlt_reg_mult_l.
  Flip.
  assumption.
  ring.
  ring.
- replace (c * b * f)%Z with (f * (c * b))%Z.  
+ replace (c * b * f)%Z with (f * (c * b))%Z.
  replace (d * (a * f))%Z with (f * (a * d))%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  apply Zlt_reg_mult_l.
  Flip.
  assumption.
@@ -1157,7 +1157,7 @@ Lemma square_pos : forall a : Z, a <> 0%Z -> (0 < a * a)%Z.
 Proof.
  intros [| p| p]; intros; [ Falsum | constructor | constructor ].
 Qed.
- 
+
 Hint Resolve square_pos: zarith.
 
 (*###########################################################################*)
@@ -1182,19 +1182,19 @@ Proof.
  intros.
  unfold Z_of_nat in |- *.
  rewrite H0.
- 
+
  apply f_equal with (A := positive) (B := Z) (f := Zpos).
  cut (P_of_succ_nat (nat_of_P p) = P_of_succ_nat (S x)).
  intro.
  rewrite P_of_succ_nat_o_nat_of_P_eq_succ in H1.
- cut (Ppred (Psucc p) = Ppred (P_of_succ_nat (S x))).
+ cut (Pos.pred (Pos.succ p) = Pos.pred (P_of_succ_nat (S x))).
  intro.
- rewrite Ppred_succ in H2.
+ rewrite Pos.pred_succ in H2.
  simpl in H2.
- rewrite Ppred_succ in H2.
+ rewrite Pos.pred_succ in H2.
  apply sym_eq.
  assumption.
- apply f_equal with (A := positive) (B := positive) (f := Ppred).
+ apply f_equal with (A := positive) (B := positive) (f := Pos.pred).
  assumption.
  apply f_equal with (f := P_of_succ_nat).
  assumption.
@@ -1222,7 +1222,7 @@ Lemma NEG_neq_ZERO : forall p : positive, Zneg p <> 0%Z.
 Proof.
  intros.
  apply Zorder.Zlt_not_eq.
- unfold Zlt in |- *.
+ unfold Z.lt in |- *.
  constructor.
 Qed.
 
@@ -1237,7 +1237,7 @@ Qed.
 Lemma nat_nat_pos : forall m n : nat, ((m + 1) * (n + 1) > 0)%Z. (*QF*)
 Proof.
  intros.
- apply Zlt_gt.
+ apply Z.lt_gt.
  cut (Z_of_nat m + 1 > 0)%Z.
  intro.
  cut (0 < Z_of_nat n + 1)%Z.
@@ -1246,24 +1246,24 @@ Proof.
  rewrite Zmult_0_r.
  intro.
  assumption.
- 
+
  apply Zlt_reg_mult_l.
  assumption.
  assumption.
- change (0 < Zsucc (Z_of_nat n))%Z in |- *.
+ change (0 < Z.succ (Z_of_nat n))%Z in |- *.
  apply Zle_lt_succ.
  change (Z_of_nat 0 <= Z_of_nat n)%Z in |- *.
  apply Znat.inj_le.
  apply le_O_n.
- apply Zlt_gt.
- change (0 < Zsucc (Z_of_nat m))%Z in |- *.
+ apply Z.lt_gt.
+ change (0 < Z.succ (Z_of_nat m))%Z in |- *.
  apply Zle_lt_succ.
  change (Z_of_nat 0 <= Z_of_nat m)%Z in |- *.
  apply Znat.inj_le.
  apply le_O_n.
 Qed.
- 
- 
+
+
 Theorem S_predn : forall m : nat, m <> 0 -> S (pred m) = m. (*QF*)
 Proof.
  intros.
@@ -1271,8 +1271,8 @@ Proof.
  intro.
  case s.
  intros.
- rewrite <- e. 
- rewrite <- pred_Sn with (n := x). 
+ rewrite <- e.
+ rewrite <- pred_Sn with (n := x).
  trivial.
  intro.
  apply False_ind.
@@ -1281,7 +1281,7 @@ Proof.
  assumption.
 Qed.
 
-Lemma absolu_1 : forall x : Z, Zabs_nat x = 0 -> x = 0%Z. (*QF*)
+Lemma absolu_1 : forall x : Z, Z.abs_nat x = 0 -> x = 0%Z. (*QF*)
 Proof.
  intros.
  case (dec_eq x 0).
@@ -1302,15 +1302,15 @@ Proof.
  apply proj1 with (B := x = 0%Z -> (x ?= 0)%Z = Datatypes.Eq).
  change ((x ?= 0)%Z = Datatypes.Eq <-> x = 0%Z) in |- *.
  apply Zcompare_Eq_iff_eq.
- 
+
  (***)
  intro.
- cut (exists h : nat, Zabs_nat x = S h).
+ cut (exists h : nat, Z.abs_nat x = S h).
  intro.
  case H3.
  rewrite H.
  exact O_S.
- 
+
  change (x < 0)%Z in H2.
  cut (0 > x)%Z.
  intro.
@@ -1324,7 +1324,7 @@ Proof.
  case H6.
  intros.
  rewrite H7.
- unfold Zabs_nat in |- *.
+ unfold Z.abs_nat in |- *.
  generalize x1.
  exact ZL4.
  cut (x = (- Zpos x0)%Z).
@@ -1335,21 +1335,21 @@ Proof.
  cut ((- - x)%Z = x).
  intro.
  rewrite <- H6.
- exact (f_equal Zopp H5). 
- apply Zopp_involutive.
+ exact (f_equal Z.opp H5).
+ apply Z.opp_involutive.
  apply Zcompare_Gt_spec.
  assumption.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
- 
+
  (***)
  intro.
- cut (exists h : nat, Zabs_nat x = S h).
+ cut (exists h : nat, Z.abs_nat x = S h).
  intro.
  case H3.
  rewrite H.
  exact O_S.
- 
+
  cut (exists p : positive, (x + - (0))%Z = Zpos p).
  simpl in |- *.
  rewrite Zplus_0_r.
@@ -1357,12 +1357,12 @@ Proof.
  case H3.
  intros.
  rewrite H4.
- unfold Zabs_nat in |- *.
+ unfold Z.abs_nat in |- *.
  generalize x0.
  exact ZL4.
  apply Zcompare_Gt_spec.
  assumption.
- 
+
  (***)
  cut ((x < 0)%Z \/ (0 < x)%Z).
  intro.
@@ -1373,14 +1373,14 @@ Proof.
  assumption.
  intro.
  right.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  assumption.
  apply not_Zeq.
  assumption.
 Qed.
 
-Lemma absolu_2 : forall x : Z, x <> 0%Z -> Zabs_nat x <> 0. (*QF*)
+Lemma absolu_2 : forall x : Z, x <> 0%Z -> Z.abs_nat x <> 0. (*QF*)
 Proof.
  intros.
  intro.
@@ -1392,7 +1392,7 @@ Qed.
 
 
 
-Lemma absolu_inject_nat : forall n : nat, Zabs_nat (Z_of_nat n) = n.
+Lemma absolu_inject_nat : forall n : nat, Z.abs_nat (Z_of_nat n) = n.
 Proof.
  simple induction n; simpl in |- *.
  reflexivity.
@@ -1404,7 +1404,7 @@ Qed.
 Lemma eq_inj : forall m n : nat, m = n :>Z -> m = n.
 Proof.
  intros.
- generalize (f_equal Zabs_nat H). 
+ generalize (f_equal Z.abs_nat H).
  intro.
  rewrite (absolu_inject_nat m) in H0.
  rewrite (absolu_inject_nat n) in H0.
@@ -1438,7 +1438,7 @@ Qed.
 
 Lemma le_absolu :
  forall x y : Z,
- (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Zabs_nat x <= Zabs_nat y.
+ (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Z.abs_nat x <= Z.abs_nat y.
 Proof.
  intros [| x| x] [| y| y] Hx Hy Hxy;
   apply le_O_n ||
@@ -1451,7 +1451,7 @@ Proof.
       | id1:(Zpos _ <= Zneg _)%Z |- _ =>
           apply False_ind; apply id1; constructor
       end).
- simpl in |- *. 
+ simpl in |- *.
  apply le_inj.
  do 2 rewrite ZL9.
  assumption.
@@ -1459,7 +1459,7 @@ Qed.
 
 Lemma lt_absolu :
  forall x y : Z,
- (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Zabs_nat x < Zabs_nat y.
+ (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Z.abs_nat x < Z.abs_nat y.
 Proof.
  intros [| x| x] [| y| y] Hx Hy Hxy; inversion Hxy;
   try
@@ -1470,13 +1470,13 @@ Proof.
        apply False_ind; apply id1; constructor
    | id1:(Zpos _ <= Zneg _)%Z |- _ =>
        apply False_ind; apply id1; constructor
-   end; simpl in |- *; apply lt_inj; repeat rewrite ZL9; 
+   end; simpl in |- *; apply lt_inj; repeat rewrite ZL9;
   assumption.
 Qed.
 
 Lemma absolu_plus :
  forall x y : Z,
- (0 <= x)%Z -> (0 <= y)%Z -> Zabs_nat (x + y) = Zabs_nat x + Zabs_nat y.
+ (0 <= x)%Z -> (0 <= y)%Z -> Z.abs_nat (x + y) = Z.abs_nat x + Z.abs_nat y.
 Proof.
  intros [| x| x] [| y| y] Hx Hy; trivial;
   try
@@ -1489,23 +1489,23 @@ Proof.
        apply False_ind; apply id1; constructor
    end.
  rewrite <- BinInt.Zpos_plus_distr.
- unfold Zabs_nat in |- *.
+ unfold Z.abs_nat in |- *.
  apply nat_of_P_plus_morphism.
 Qed.
 
 Lemma pred_absolu :
- forall x : Z, (0 < x)%Z -> pred (Zabs_nat x) = Zabs_nat (x - 1).
+ forall x : Z, (0 < x)%Z -> pred (Z.abs_nat x) = Z.abs_nat (x - 1).
 Proof.
  intros x Hx.
  generalize (Z_lt_lt_S_eq_dec 0 x Hx); simpl in |- *; intros [H1| H1];
-  [ replace (Zabs_nat x) with (Zabs_nat (x - 1 + 1));
+  [ replace (Z.abs_nat x) with (Z.abs_nat (x - 1 + 1));
      [ idtac | apply f_equal with Z; auto with zarith ];
      rewrite absolu_plus;
-     [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; omega
+     [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; omega
      | auto with zarith
      | intro; discriminate ]
   | rewrite <- H1; reflexivity ].
-Qed. 
+Qed.
 
 Definition pred_nat : forall (x : Z) (Hx : (0 < x)%Z), nat.
 intros [| px| px] Hx; try abstract (discriminate Hx).
@@ -1535,7 +1535,7 @@ Proof.
 Qed.
 
 Lemma absolu_pred_nat :
- forall (m : Z) (Hm : (0 < m)%Z), S (pred_nat m Hm) = Zabs_nat m.
+ forall (m : Z) (Hm : (0 < m)%Z), S (pred_nat m Hm) = Z.abs_nat m.
 Proof.
  intros [| px| px] Hx; try discriminate Hx.
  unfold pred_nat in |- *.
@@ -1545,7 +1545,7 @@ Proof.
 Qed.
 
 Lemma pred_nat_absolu :
- forall (m : Z) (Hm : (0 < m)%Z), pred_nat m Hm = Zabs_nat (m - 1).
+ forall (m : Z) (Hm : (0 < m)%Z), pred_nat m Hm = Z.abs_nat (m - 1).
 Proof.
  intros [| px| px] Hx; try discriminate Hx.
  unfold pred_nat in |- *.
@@ -1557,15 +1557,15 @@ Lemma minus_pred_nat :
  S (pred_nat n Hn) - S (pred_nat m Hm) = S (pred_nat (n - m) Hnm).
 Proof.
  intros.
- simpl in |- *.  
+ simpl in |- *.
  destruct n; try discriminate Hn.
  destruct m; try discriminate Hm.
  unfold pred_nat at 1 2 in |- *.
  rewrite minus_pred; try apply lt_O_nat_of_P.
  apply eq_inj.
- rewrite <- pred_nat_unfolded. 
+ rewrite <- pred_nat_unfolded.
  rewrite Znat.inj_minus1.
- repeat rewrite ZL9. 
+ repeat rewrite ZL9.
  reflexivity.
  apply le_inj.
  apply Zlt_le_weak.
@@ -1581,13 +1581,13 @@ Qed.
 
 
 Lemma Zsgn_1 :
- forall x : Z, {Zsgn x = 0%Z} + {Zsgn x = 1%Z} + {Zsgn x = (-1)%Z}. (*QF*)
+ forall x : Z, {Z.sgn x = 0%Z} + {Z.sgn x = 1%Z} + {Z.sgn x = (-1)%Z}. (*QF*)
 Proof.
  intros.
  case x.
  left.
  left.
- unfold Zsgn in |- *.
+ unfold Z.sgn in |- *.
  reflexivity.
  intro.
  simpl in |- *.
@@ -1601,13 +1601,13 @@ Proof.
 Qed.
 
 
-Lemma Zsgn_2 : forall x : Z, Zsgn x = 0%Z -> x = 0%Z.   (*QF*)
+Lemma Zsgn_2 : forall x : Z, Z.sgn x = 0%Z -> x = 0%Z.   (*QF*)
 Proof.
  intros [| p1| p1]; simpl in |- *; intro H; constructor || discriminate H.
 Qed.
 
 
-Lemma Zsgn_3 : forall x : Z, x <> 0%Z -> Zsgn x <> 0%Z.   (*QF*)
+Lemma Zsgn_3 : forall x : Z, x <> 0%Z -> Z.sgn x <> 0%Z.   (*QF*)
 Proof.
  intro.
  case x.
@@ -1626,21 +1626,21 @@ Qed.
 
 
 
-Theorem Zsgn_4 : forall a : Z, a = (Zsgn a * Zabs_nat a)%Z.  (*QF*)
+Theorem Zsgn_4 : forall a : Z, a = (Z.sgn a * Z.abs_nat a)%Z.  (*QF*)
 Proof.
  intro.
  case a.
  simpl in |- *.
  reflexivity.
  intro.
- unfold Zsgn in |- *.
- unfold Zabs_nat in |- *.
+ unfold Z.sgn in |- *.
+ unfold Z.abs_nat in |- *.
  rewrite Zmult_1_l.
  symmetry  in |- *.
  apply ZL9.
  intros.
- unfold Zsgn in |- *.
- unfold Zabs_nat in |- *.
+ unfold Z.sgn in |- *.
+ unfold Z.abs_nat in |- *.
  rewrite ZL9.
  constructor.
 Qed.
@@ -1650,7 +1650,7 @@ Theorem Zsgn_5 :
  forall a b x y : Z,
  x <> 0%Z ->
  y <> 0%Z ->
- (Zsgn a * x)%Z = (Zsgn b * y)%Z -> (Zsgn a * y)%Z = (Zsgn b * x)%Z.  (*QF*)
+ (Z.sgn a * x)%Z = (Z.sgn b * y)%Z -> (Z.sgn a * y)%Z = (Z.sgn b * x)%Z.  (*QF*)
 Proof.
  intros a b x y H H0.
  case a.
@@ -1660,7 +1660,7 @@ Proof.
  trivial.
 
  intro.
- unfold Zsgn in |- *.
+ unfold Z.sgn in |- *.
  intro.
  rewrite Zmult_1_l in H1.
  simpl in H1.
@@ -1669,11 +1669,11 @@ Proof.
  symmetry  in |- *.
  assumption.
  intro.
- unfold Zsgn in |- *.
+ unfold Z.sgn in |- *.
  intro.
  apply False_ind.
  apply H0.
- apply Zopp_inj.
+ apply Z.opp_inj.
  simpl in |- *.
  transitivity (-1 * y)%Z.
  constructor.
@@ -1683,13 +1683,13 @@ Proof.
  simpl in |- *.
  reflexivity.
  intro.
- unfold Zsgn at 1 in |- *.
- unfold Zsgn at 2 in |- *.
+ unfold Z.sgn at 1 in |- *.
+ unfold Z.sgn at 2 in |- *.
  intro.
  transitivity y.
  rewrite Zmult_1_l.
  reflexivity.
- transitivity (Zsgn b * (Zsgn b * y))%Z.
+ transitivity (Z.sgn b * (Z.sgn b * y))%Z.
  case (Zsgn_1 b).
  intro.
  case s.
@@ -1712,20 +1712,20 @@ Proof.
  rewrite H1.
  reflexivity.
  intro.
- unfold Zsgn at 1 in |- *.
- unfold Zsgn at 2 in |- *.
+ unfold Z.sgn at 1 in |- *.
+ unfold Z.sgn at 2 in |- *.
  intro.
- transitivity (Zsgn b * (-1 * (Zsgn b * y)))%Z.
+ transitivity (Z.sgn b * (-1 * (Z.sgn b * y)))%Z.
  case (Zsgn_1 b).
  intros.
  case s.
  intro.
  apply False_ind.
  apply H.
- apply Zopp_inj.
+ apply Z.opp_inj.
  transitivity (-1 * x)%Z.
  ring.
- unfold Zopp in |- *.
+ unfold Z.opp in |- *.
  rewrite e in H1.
  transitivity (0 * y)%Z.
  assumption.
@@ -1741,7 +1741,7 @@ Proof.
  ring.
 Qed.
 
-Lemma Zsgn_6 : forall x : Z, x = 0%Z -> Zsgn x = 0%Z.
+Lemma Zsgn_6 : forall x : Z, x = 0%Z -> Z.sgn x = 0%Z.
 Proof.
  intros.
  rewrite H.
@@ -1750,44 +1750,44 @@ Proof.
 Qed.
 
 
-Lemma Zsgn_7 : forall x : Z, (x > 0)%Z -> Zsgn x = 1%Z.
+Lemma Zsgn_7 : forall x : Z, (x > 0)%Z -> Z.sgn x = 1%Z.
 Proof.
  intro.
  case x.
  intro.
  apply False_ind.
- apply (Zlt_irrefl 0).
+ apply (Z.lt_irrefl 0).
  Flip.
  intros.
  simpl in |- *.
  reflexivity.
  intros.
  apply False_ind.
- apply (Zlt_irrefl (Zneg p)).
- apply Zlt_trans with 0%Z.
+ apply (Z.lt_irrefl (Zneg p)).
+ apply Z.lt_trans with 0%Z.
  constructor.
  Flip.
 Qed.
 
 
-Lemma Zsgn_7' : forall x : Z, (0 < x)%Z -> Zsgn x = 1%Z.
+Lemma Zsgn_7' : forall x : Z, (0 < x)%Z -> Z.sgn x = 1%Z.
 Proof.
  intros; apply Zsgn_7; Flip.
 Qed.
 
 
-Lemma Zsgn_8 : forall x : Z, (x < 0)%Z -> Zsgn x = (-1)%Z.
+Lemma Zsgn_8 : forall x : Z, (x < 0)%Z -> Z.sgn x = (-1)%Z.
 Proof.
  intro.
  case x.
  intro.
  apply False_ind.
- apply (Zlt_irrefl 0).
+ apply (Z.lt_irrefl 0).
  assumption.
  intros.
  apply False_ind.
- apply (Zlt_irrefl 0).
- apply Zlt_trans with (Zpos p).
+ apply (Z.lt_irrefl 0).
+ apply Z.lt_trans with (Zpos p).
  constructor.
  assumption.
  intros.
@@ -1795,7 +1795,7 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zsgn_9 : forall x : Z, Zsgn x = 1%Z -> (0 < x)%Z.
+Lemma Zsgn_9 : forall x : Z, Z.sgn x = 1%Z -> (0 < x)%Z.
 Proof.
  intro.
  case x.
@@ -1809,8 +1809,8 @@ Proof.
  apply False_ind.
  discriminate.
 Qed.
- 
-Lemma Zsgn_10 : forall x : Z, Zsgn x = (-1)%Z -> (x < 0)%Z.
+
+Lemma Zsgn_10 : forall x : Z, Z.sgn x = (-1)%Z -> (x < 0)%Z.
 Proof.
  intro.
  case x.
@@ -1822,9 +1822,9 @@ Proof.
  discriminate.
  intros.
  constructor.
-Qed. 
+Qed.
 
-Lemma Zsgn_11 : forall x : Z, (Zsgn x < 0)%Z -> (x < 0)%Z.
+Lemma Zsgn_11 : forall x : Z, (Z.sgn x < 0)%Z -> (x < 0)%Z.
 Proof.
  intros.
  apply Zsgn_10.
@@ -1833,7 +1833,7 @@ Proof.
  apply False_ind.
  case s.
  intro.
- generalize (Zorder.Zlt_not_eq _ _ H). 
+ generalize (Zorder.Zlt_not_eq _ _ H).
  intro.
  apply (H0 e).
  intro.
@@ -1842,9 +1842,9 @@ Proof.
  intro.
  discriminate.
  trivial.
-Qed. 
+Qed.
 
-Lemma Zsgn_12 : forall x : Z, (0 < Zsgn x)%Z -> (0 < x)%Z.
+Lemma Zsgn_12 : forall x : Z, (0 < Z.sgn x)%Z -> (0 < x)%Z.
 Proof.
  intros.
  apply Zsgn_9.
@@ -1852,7 +1852,7 @@ Proof.
  intro.
  case s.
  intro.
- generalize (Zorder.Zlt_not_eq _ _ H). 
+ generalize (Zorder.Zlt_not_eq _ _ H).
  intro.
  generalize (sym_eq e).
  intro.
@@ -1865,78 +1865,78 @@ Proof.
  intro.
  apply False_ind.
  discriminate.
-Qed.   
+Qed.
 
-Lemma Zsgn_13 : forall x : Z, (0 <= Zsgn x)%Z -> (0 <= x)%Z.
+Lemma Zsgn_13 : forall x : Z, (0 <= Z.sgn x)%Z -> (0 <= x)%Z.
 Proof.
- intros. 
- case (Z_le_lt_eq_dec 0 (Zsgn x) H).
+ intros.
+ case (Z_le_lt_eq_dec 0 (Z.sgn x) H).
  intro.
  apply Zlt_le_weak.
  apply Zsgn_12.
- assumption. 
+ assumption.
  intro.
- assert (x = 0%Z). 
+ assert (x = 0%Z).
  apply Zsgn_2.
  symmetry  in |- *.
  assumption.
  rewrite H0.
- apply Zle_refl.
+ apply Z.le_refl.
 Qed.
 
-Lemma Zsgn_14 : forall x : Z, (Zsgn x <= 0)%Z -> (x <= 0)%Z.
+Lemma Zsgn_14 : forall x : Z, (Z.sgn x <= 0)%Z -> (x <= 0)%Z.
 Proof.
- intros. 
- case (Z_le_lt_eq_dec (Zsgn x) 0 H).
+ intros.
+ case (Z_le_lt_eq_dec (Z.sgn x) 0 H).
  intro.
  apply Zlt_le_weak.
  apply Zsgn_11.
- assumption. 
+ assumption.
  intro.
- assert (x = 0%Z). 
+ assert (x = 0%Z).
  apply Zsgn_2.
  assumption.
  rewrite H0.
- apply Zle_refl.
+ apply Z.le_refl.
 Qed.
 
-Lemma Zsgn_15 : forall x y : Z, Zsgn (x * y) = (Zsgn x * Zsgn y)%Z.
+Lemma Zsgn_15 : forall x y : Z, Z.sgn (x * y) = (Z.sgn x * Z.sgn y)%Z.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; constructor.
 Qed.
 
 Lemma Zsgn_16 :
  forall x y : Z,
- Zsgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}.
+ Z.sgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right ]; repeat split.
-Qed. 
+Qed.
 
 Lemma Zsgn_17 :
  forall x y : Z,
- Zsgn (x * y) = (-1)%Z -> {(0 < x)%Z /\ (y < 0)%Z} + {(x < 0)%Z /\ (0 < y)%Z}.
+ Z.sgn (x * y) = (-1)%Z -> {(0 < x)%Z /\ (y < 0)%Z} + {(x < 0)%Z /\ (0 < y)%Z}.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right ]; repeat split.
-Qed. 
+Qed.
 
-Lemma Zsgn_18 : forall x y : Z, Zsgn (x * y) = 0%Z -> {x = 0%Z} + {y = 0%Z}.
+Lemma Zsgn_18 : forall x y : Z, Z.sgn (x * y) = 0%Z -> {x = 0%Z} + {y = 0%Z}.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right | right ]; constructor.
-Qed. 
+Qed.
 
 
 
-Lemma Zsgn_19 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 < x + y)%Z.
+Lemma Zsgn_19 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 < x + y)%Z.
 Proof.
  Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   discriminate H || (constructor || apply Zsgn_12; assumption).
 Qed.
 
-Lemma Zsgn_20 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x + y < 0)%Z.
+Lemma Zsgn_20 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x + y < 0)%Z.
 Proof.
  Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
@@ -1944,43 +1944,43 @@ Proof.
 Qed.
 
 
-Lemma Zsgn_21 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= x)%Z.
+Lemma Zsgn_21 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 <= x)%Z.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
   discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_22 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x <= 0)%Z.
+Lemma Zsgn_22 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x <= 0)%Z.
 Proof.
  Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
   discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_23 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= y)%Z.
+Lemma Zsgn_23 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 <= y)%Z.
 Proof.
  intros [|p1|p1] [|p2|p2]; simpl in |- *;
   intros H H0; discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_24 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (y <= 0)%Z.
+Lemma Zsgn_24 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (y <= 0)%Z.
 Proof.
  intros [|p1|p1] [|p2|p2]; simpl in |- *;
   intros H H0; discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_25 : forall x : Z, Zsgn (- x) = (- Zsgn x)%Z.
+Lemma Zsgn_25 : forall x : Z, Z.sgn (- x) = (- Z.sgn x)%Z.
 Proof.
  intros [| p1| p1]; simpl in |- *; reflexivity.
 Qed.
 
 
-Lemma Zsgn_26 : forall x : Z, (0 < x)%Z -> (0 < Zsgn x)%Z.
+Lemma Zsgn_26 : forall x : Z, (0 < x)%Z -> (0 < Z.sgn x)%Z.
 Proof.
  intros [| p| p] Hp; trivial.
 Qed.
 
-Lemma Zsgn_27 : forall x : Z, (x < 0)%Z -> (Zsgn x < 0)%Z.
+Lemma Zsgn_27 : forall x : Z, (x < 0)%Z -> (Z.sgn x < 0)%Z.
 Proof.
  intros [| p| p] Hp; trivial.
 Qed.
@@ -1994,7 +1994,7 @@ Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8
 (** Properties of Zabs                                                       *)
 (*###########################################################################*)
 
-Lemma Zabs_1 : forall z p : Z, (Zabs z < p)%Z -> (z < p)%Z /\ (- p < z)%Z.
+Lemma Zabs_1 : forall z p : Z, (Z.abs z < p)%Z -> (z < p)%Z /\ (- p < z)%Z.
 Proof.
  intros z p.
  case z.
@@ -2003,25 +2003,25 @@ Proof.
  split.
  assumption.
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
- replace (-1)%Z with (Zpred 0).
+ replace (-1)%Z with (Z.pred 0).
  apply Zlt_pred.
  simpl; trivial.
  ring_simplify (-1 * - p)%Z (-1 * 0)%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
 
  intros.
  simpl in H.
  split.
  assumption.
- apply Zlt_trans with (m := 0%Z).
+ apply Z.lt_trans with (m := 0%Z).
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
- replace (-1)%Z with (Zpred 0).
+ replace (-1)%Z with (Z.pred 0).
  apply Zlt_pred.
  simpl; trivial.
  ring_simplify (-1 * - p)%Z (-1 * 0)%Z.
- apply Zlt_gt.
- apply Zlt_trans with (m := Zpos p0).
+ apply Z.lt_gt.
+ apply Z.lt_trans with (m := Zpos p0).
  constructor.
  assumption.
  constructor.
@@ -2029,28 +2029,28 @@ Proof.
  intros.
  simpl in H.
  split.
- apply Zlt_trans with (m := Zpos p0).
+ apply Z.lt_trans with (m := Zpos p0).
  constructor.
  assumption.
- 
+
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
- replace (-1)%Z with (Zpred 0).
+ replace (-1)%Z with (Z.pred 0).
  apply Zlt_pred.
  simpl;trivial.
  ring_simplify (-1 * - p)%Z.
  replace (-1 * Zneg p0)%Z with (- Zneg p0)%Z.
- replace (- Zneg p0)%Z with (Zpos p0). 
- apply Zlt_gt.
+ replace (- Zneg p0)%Z with (Zpos p0).
+ apply Z.lt_gt.
  assumption.
  symmetry  in |- *.
  apply Zopp_neg.
- rewrite Zopp_mult_distr_l_reverse with (n := 1%Z). 
+ rewrite Zopp_mult_distr_l_reverse with (n := 1%Z).
  simpl in |- *.
  constructor.
 Qed.
 
 
-Lemma Zabs_2 : forall z p : Z, (Zabs z > p)%Z -> (z > p)%Z \/ (- p > z)%Z.
+Lemma Zabs_2 : forall z p : Z, (Z.abs z > p)%Z -> (z > p)%Z \/ (- p > z)%Z.
 Proof.
  intros z p.
  case z.
@@ -2067,7 +2067,7 @@ Proof.
  intros.
  simpl in H.
  right.
- apply Zlt_gt.
+ apply Z.lt_gt.
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
  constructor.
  ring_simplify (-1 * - p)%Z.
@@ -2076,22 +2076,22 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zabs_3 : forall z p : Z, (z < p)%Z /\ (- p < z)%Z -> (Zabs z < p)%Z.
+Lemma Zabs_3 : forall z p : Z, (z < p)%Z /\ (- p < z)%Z -> (Z.abs z < p)%Z.
 Proof.
  intros z p.
  case z.
-  intro. 
+  intro.
   simpl in |- *.
   elim H.
   intros.
   assumption.
-  
+
   intros.
   elim H.
   intros.
   simpl in |- *.
   assumption.
-  
+
   intros.
   elim H.
   intros.
@@ -2100,14 +2100,14 @@ Proof.
   constructor.
   replace (-1 * Zpos p0)%Z with (Zneg p0).
   replace (-1 * p)%Z with (- p)%Z.
-  apply Zlt_gt.
+  apply Z.lt_gt.
   assumption.
-  ring.  
+  ring.
   simpl in |- *.
   reflexivity.
 Qed.
 
-Lemma Zabs_4 : forall z p : Z, (Zabs z < p)%Z -> (- p < z < p)%Z.
+Lemma Zabs_4 : forall z p : Z, (Z.abs z < p)%Z -> (- p < z < p)%Z.
 Proof.
  intros.
  split.
@@ -2118,28 +2118,28 @@ Proof.
  apply Zabs_1.
  assumption.
 Qed.
- 
 
-Lemma Zabs_5 : forall z p : Z, (Zabs z <= p)%Z -> (- p <= z <= p)%Z.
+
+Lemma Zabs_5 : forall z p : Z, (Z.abs z <= p)%Z -> (- p <= z <= p)%Z.
 Proof.
  intros.
  split.
- replace (- p)%Z with (Zsucc (- Zsucc p)).
+ replace (- p)%Z with (Z.succ (- Z.succ p)).
  apply Zlt_le_succ.
- apply proj2 with (A := (z < Zsucc p)%Z).
+ apply proj2 with (A := (z < Z.succ p)%Z).
  apply Zabs_1.
  apply Zle_lt_succ.
  assumption.
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  ring.
  apply Zlt_succ_le.
- apply proj1 with (B := (- Zsucc p < z)%Z).
+ apply proj1 with (B := (- Z.succ p < z)%Z).
  apply Zabs_1.
  apply Zle_lt_succ.
  assumption.
 Qed.
 
-Lemma Zabs_6 : forall z p : Z, (Zabs z <= p)%Z -> (z <= p)%Z.
+Lemma Zabs_6 : forall z p : Z, (Z.abs z <= p)%Z -> (z <= p)%Z.
 Proof.
  intros.
  apply proj2 with (A := (- p <= z)%Z).
@@ -2147,7 +2147,7 @@ Proof.
  assumption.
 Qed.
 
-Lemma Zabs_7 : forall z p : Z, (Zabs z <= p)%Z -> (- p <= z)%Z.
+Lemma Zabs_7 : forall z p : Z, (Z.abs z <= p)%Z -> (- p <= z)%Z.
 Proof.
  intros.
  apply proj1 with (B := (z <= p)%Z).
@@ -2155,7 +2155,7 @@ Proof.
  assumption.
 Qed.
 
-Lemma Zabs_8 : forall z p : Z, (- p <= z <= p)%Z -> (Zabs z <= p)%Z.
+Lemma Zabs_8 : forall z p : Z, (- p <= z <= p)%Z -> (Z.abs z <= p)%Z.
 Proof.
  intros.
  apply Zlt_succ_le.
@@ -2165,14 +2165,14 @@ Proof.
  split.
  apply Zle_lt_succ.
  assumption.
- apply Zlt_le_trans with (m := (- p)%Z).
- apply Zgt_lt. 
+ apply Z.lt_le_trans with (m := (- p)%Z).
+ apply Z.gt_lt.
  apply Zlt_opp.
  apply Zlt_succ.
  assumption.
 Qed.
 
-Lemma Zabs_min : forall z : Z, Zabs z = Zabs (- z).
+Lemma Zabs_min : forall z : Z, Z.abs z = Z.abs (- z).
 Proof.
  intro.
  case z.
@@ -2187,67 +2187,67 @@ Proof.
 Qed.
 
 Lemma Zabs_9 :
- forall z p : Z, (0 <= p)%Z -> (p < z)%Z \/ (z < - p)%Z -> (p < Zabs z)%Z.
+ forall z p : Z, (0 <= p)%Z -> (p < z)%Z \/ (z < - p)%Z -> (p < Z.abs z)%Z.
 Proof.
  intros.
  case H0.
  intro.
- replace (Zabs z) with z.
+ replace (Z.abs z) with z.
  assumption.
  symmetry  in |- *.
- apply Zabs_eq.
+ apply Z.abs_eq.
  apply Zlt_le_weak.
- apply Zle_lt_trans with (m := p).
+ apply Z.le_lt_trans with (m := p).
  assumption.
  assumption.
  intro.
- cut (Zabs z = (- z)%Z).
+ cut (Z.abs z = (- z)%Z).
  intro.
  rewrite H2.
  apply Zmin_cancel_Zlt.
  ring_simplify (- - z)%Z.
  assumption.
  rewrite Zabs_min.
- apply Zabs_eq.
+ apply Z.abs_eq.
  apply Zlt_le_weak.
- apply Zle_lt_trans with (m := p).
+ apply Z.le_lt_trans with (m := p).
  assumption.
  apply Zmin_cancel_Zlt.
  ring_simplify (- - z)%Z.
  assumption.
 Qed.
 
-Lemma Zabs_10 : forall z : Z, (0 <= Zabs z)%Z.
+Lemma Zabs_10 : forall z : Z, (0 <= Z.abs z)%Z.
 Proof.
  intro.
  case (Z_zerop z).
  intro.
  rewrite e.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  intro.
  case (not_Zeq z 0 n).
  intro.
  apply Zlt_le_weak.
  apply Zabs_9.
- apply Zle_refl.
+ apply Z.le_refl.
  simpl in |- *.
  right.
  assumption.
  intro.
  apply Zlt_le_weak.
  apply Zabs_9.
- apply Zle_refl.
+ apply Z.le_refl.
  simpl in |- *.
  left.
  assumption.
 Qed.
 
-Lemma Zabs_11 : forall z : Z, z <> 0%Z -> (0 < Zabs z)%Z.
+Lemma Zabs_11 : forall z : Z, z <> 0%Z -> (0 < Z.abs z)%Z.
 Proof.
  intros.
  apply Zabs_9.
- apply Zle_refl.
+ apply Z.le_refl.
  simpl in |- *.
  apply not_Zeq.
  intro.
@@ -2256,14 +2256,14 @@ Proof.
  assumption.
 Qed.
 
-Lemma Zabs_12 : forall z m : Z, (m < Zabs z)%Z -> {(m < z)%Z} + {(z < - m)%Z}.
+Lemma Zabs_12 : forall z m : Z, (m < Z.abs z)%Z -> {(m < z)%Z} + {(z < - m)%Z}.
 Proof.
  intros [| p| p] m; simpl in |- *; intros H;
-  [ left | left | right; apply Zmin_cancel_Zlt; rewrite Zopp_involutive ];
+  [ left | left | right; apply Zmin_cancel_Zlt; rewrite Z.opp_involutive ];
   assumption.
 Qed.
 
-Lemma Zabs_mult : forall z p : Z, Zabs (z * p) = (Zabs z * Zabs p)%Z.
+Lemma Zabs_mult : forall z p : Z, Z.abs (z * p) = (Z.abs z * Z.abs p)%Z.
 Proof.
  intros.
  case z.
@@ -2290,22 +2290,22 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zabs_plus : forall z p : Z, (Zabs (z + p) <= Zabs z + Zabs p)%Z.
+Lemma Zabs_plus : forall z p : Z, (Z.abs (z + p) <= Z.abs z + Z.abs p)%Z.
 Proof.
  intros.
  case z.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  case p.
  intro.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
- unfold Zabs at 2 in |- *.
- unfold Zabs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
  apply Zabs_8.
  split.
  apply Zplus_le_reg_l with (Zpos p1 - Zneg p0)%Z.
@@ -2322,17 +2322,17 @@ Proof.
  ring.
  ring.
  apply Zplus_le_compat.
- apply Zle_refl.
+ apply Z.le_refl.
  apply Zlt_le_weak.
  constructor.
- 
+
  case p.
  simpl in |- *.
  intro.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
- unfold Zabs at 2 in |- *.
- unfold Zabs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
  apply Zabs_8.
  split.
  apply Zplus_le_reg_l with (Zpos p1 + Zneg p0)%Z.
@@ -2360,13 +2360,13 @@ Proof.
  apply Zplus_le_compat.
  apply Zlt_le_weak.
  constructor.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
 Qed.
 
-Lemma Zabs_neg : forall z : Z, (z <= 0)%Z -> Zabs z = (- z)%Z.
+Lemma Zabs_neg : forall z : Z, (z <= 0)%Z -> Z.abs z = (- z)%Z.
 Proof.
  intro.
  case z.
@@ -2383,11 +2383,11 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zle_Zabs: forall z, (z <= Zabs z)%Z.
+Lemma Zle_Zabs: forall z, (z <= Z.abs z)%Z.
 Proof.
- intros [|z|z]; simpl; auto with zarith; apply Zle_neg_pos. 
+ intros [|z|z]; simpl; auto with zarith; apply Zle_neg_pos.
 Qed.
- 
+
 Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9
   Zabs_10 Zabs_11 Zabs_12 Zabs_min Zabs_neg Zabs_mult Zabs_plus Zle_Zabs: zarith.
 
@@ -2400,7 +2400,7 @@ Lemma Zind :
  forall (P : Z -> Prop) (p : Z),
  P p ->
  (forall q : Z, (p <= q)%Z -> P q -> P (q + 1)%Z) ->
- forall q : Z, (p <= q)%Z -> P q. 
+ forall q : Z, (p <= q)%Z -> P q.
 Proof.
  intros P p.
  intro.
@@ -2426,14 +2426,14 @@ Proof.
  replace (p + Z_of_nat (S k))%Z with (p + k + 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (Z_of_nat 0). 
+ replace (- p + p)%Z with (Z_of_nat 0).
  ring_simplify (- p + (p + Z_of_nat k))%Z.
  apply Znat.inj_le.
  apply le_O_n.
- ring_simplify; auto with arith. 
+ ring_simplify; auto with arith.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  ring.
  intros.
  cut (exists k : nat, (q - p)%Z = Z_of_nat k).
@@ -2457,7 +2457,7 @@ Lemma Zrec :
  forall (P : Z -> Set) (p : Z),
  P p ->
  (forall q : Z, (p <= q)%Z -> P q -> P (q + 1)%Z) ->
- forall q : Z, (p <= q)%Z -> P q. 
+ forall q : Z, (p <= q)%Z -> P q.
 Proof.
  intros F p.
  intro.
@@ -2483,7 +2483,7 @@ Proof.
  replace (p + Z_of_nat (S k))%Z with (p + k + 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (Z_of_nat 0). 
+ replace (- p + p)%Z with (Z_of_nat 0).
  replace (- p + (p + Z_of_nat k))%Z with (Z_of_nat k).
  apply Znat.inj_le.
  apply le_O_n.
@@ -2491,7 +2491,7 @@ Proof.
  rewrite Zplus_opp_l; reflexivity.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  apply Zplus_assoc_reverse.
  intros.
  cut {k : nat | (q - p)%Z = Z_of_nat k}.
@@ -2540,14 +2540,14 @@ Proof.
  replace (p - 0)%Z with p.
  assumption.
  unfold Zminus in |- *.
- unfold Zopp in |- *.
+ unfold Z.opp in |- *.
  rewrite Zplus_0_r; reflexivity.
  replace (p - Z_of_nat (S k))%Z with (p - k - 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (- Z_of_nat 0)%Z. 
+ replace (- p + p)%Z with (- Z_of_nat 0)%Z.
  replace (- p + (p - Z_of_nat k))%Z with (- Z_of_nat k)%Z.
- apply Zge_le.
+ apply Z.ge_le.
  apply Zge_opp.
  apply Znat.inj_le.
  apply le_O_n.
@@ -2555,7 +2555,7 @@ Proof.
  rewrite Zplus_opp_l; reflexivity.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  unfold Zminus at 1 2 in |- *.
  rewrite Zplus_assoc_reverse.
  rewrite <- Zopp_plus_distr.
@@ -2567,16 +2567,16 @@ Proof.
  intro k.
  intros.
  exists k.
- apply Zopp_inj. 
+ apply Z.opp_inj.
  apply Zplus_reg_l with (n := p).
- replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k). 
+ replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k).
  rewrite <- e.
  reflexivity.
  unfold Zminus in |- *.
  rewrite Zopp_plus_distr.
  rewrite Zplus_assoc.
  rewrite Zplus_opp_r.
- rewrite Zopp_involutive.
+ rewrite Z.opp_involutive.
  reflexivity.
  apply Z_of_nat_complete_inf.
  unfold Zminus in |- *.
@@ -2615,17 +2615,17 @@ Proof.
  replace (p - Z_of_nat (S k))%Z with (p - k - 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (- Z_of_nat 0)%Z. 
+ replace (- p + p)%Z with (- Z_of_nat 0)%Z.
  replace (- p + (p - Z_of_nat k))%Z with (- Z_of_nat k)%Z.
- apply Zge_le.
+ apply Z.ge_le.
  apply Zge_opp.
  apply Znat.inj_le.
  apply le_O_n.
- ring. 
+ ring.
  ring_simplify; auto with arith.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  ring.
  intros.
  cut (exists k : nat, (p - q)%Z = Z_of_nat k).
@@ -2634,9 +2634,9 @@ Proof.
  intro k.
  intros.
  exists k.
- apply Zopp_inj. 
+ apply Z.opp_inj.
  apply Zplus_reg_l with (n := p).
- replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k). 
+ replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k).
  rewrite <- H3.
  ring.
  ring.
@@ -2654,44 +2654,44 @@ Proof.
  intros P p WF_ind_step q Hq.
  cut (forall x : Z, (p <= x)%Z -> forall y : Z, (p <= y < x)%Z -> P y).
  intro.
- apply (H (Zsucc q)).
+ apply (H (Z.succ q)).
  apply Zle_le_succ.
  assumption.
- 
+
  split; [ assumption | exact (Zlt_succ q) ].
 
- intros x0 Hx0; generalize Hx0; pattern x0 in |- *. 
+ intros x0 Hx0; generalize Hx0; pattern x0 in |- *.
  apply Zrec with (p := p).
  intros.
  absurd (p <= p)%Z.
  apply Zgt_not_le.
  apply Zgt_le_trans with (m := y).
- apply Zlt_gt.
+ apply Z.lt_gt.
  elim H.
  intros.
  assumption.
  elim H.
  intros.
  assumption.
- apply Zle_refl.
+ apply Z.le_refl.
 
- intros. 
- apply WF_ind_step. 
+ intros.
+ apply WF_ind_step.
  intros.
  apply (H0 H).
- split. 
+ split.
  elim H2.
  intros.
  assumption.
- apply Zlt_le_trans with y. 
+ apply Z.lt_le_trans with y.
  elim H2.
  intros.
  assumption.
- apply Zgt_succ_le. 
- apply Zlt_gt. 
+ apply Zgt_succ_le.
+ apply Z.lt_gt.
  elim H1.
  intros.
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  assumption.
  assumption.
 Qed.
@@ -2744,44 +2744,44 @@ Proof.
  intros P p WF_ind_step q Hq.
  cut (forall x : Z, (p <= x)%Z -> forall y : Z, (p <= y < x)%Z -> P y).
  intro.
- apply (H (Zsucc q)).
+ apply (H (Z.succ q)).
  apply Zle_le_succ.
  assumption.
- 
+
  split; [ assumption | exact (Zlt_succ q) ].
 
- intros x0 Hx0; generalize Hx0; pattern x0 in |- *. 
+ intros x0 Hx0; generalize Hx0; pattern x0 in |- *.
  apply Zind with (p := p).
  intros.
  absurd (p <= p)%Z.
  apply Zgt_not_le.
  apply Zgt_le_trans with (m := y).
- apply Zlt_gt.
+ apply Z.lt_gt.
  elim H.
  intros.
  assumption.
  elim H.
  intros.
  assumption.
- apply Zle_refl.
+ apply Z.le_refl.
 
- intros. 
- apply WF_ind_step. 
+ intros.
+ apply WF_ind_step.
  intros.
  apply (H0 H).
- split. 
+ split.
  elim H2.
  intros.
  assumption.
- apply Zlt_le_trans with y. 
+ apply Z.lt_le_trans with y.
  elim H2.
  intros.
  assumption.
- apply Zgt_succ_le. 
- apply Zlt_gt. 
+ apply Zgt_succ_le.
+ apply Z.lt_gt.
  elim H1.
  intros.
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  assumption.
  assumption.
 Qed.
@@ -2830,16 +2830,16 @@ Qed.
 (** Properties of Zmax                                                       *)
 (*###########################################################################*)
 
-Definition Zmax (n m : Z) := (n + m - Zmin n m)%Z.
+Definition Zmax (n m : Z) := (n + m - Z.min n m)%Z.
 
 Lemma ZmaxSS : forall n m : Z, (Zmax n m + 1)%Z = Zmax (n + 1) (m + 1).
 Proof.
  intros.
  unfold Zmax in |- *.
- replace (Zmin (n + 1) (m + 1)) with (Zmin n m + 1)%Z.
+ replace (Z.min (n + 1) (m + 1)) with (Z.min n m + 1)%Z.
  ring.
  symmetry  in |- *.
- change (Zmin (Zsucc n) (Zsucc m) = Zsucc (Zmin n m)) in |- *.
+ change (Z.min (Z.succ n) (Z.succ m) = Z.succ (Z.min n m)) in |- *.
  symmetry  in |- *.
  apply Zmin_SS.
 Qed.
@@ -2848,29 +2848,29 @@ Lemma Zle_max_l : forall n m : Z, (n <= Zmax n m)%Z.
 Proof.
  intros.
  unfold Zmax in |- *.
- apply Zplus_le_reg_l with (p := (- n + Zmin n m)%Z).
- ring_simplify (- n + Zmin n m + n)%Z.
- ring_simplify (- n + Zmin n m + (n + m - Zmin n m))%Z.
- apply Zle_min_r.
+ apply Zplus_le_reg_l with (p := (- n + Z.min n m)%Z).
+ ring_simplify (- n + Z.min n m + n)%Z.
+ ring_simplify (- n + Z.min n m + (n + m - Z.min n m))%Z.
+ apply Z.le_min_r.
 Qed.
 
 Lemma Zle_max_r : forall n m : Z, (m <= Zmax n m)%Z.
 Proof.
  intros.
  unfold Zmax in |- *.
- apply Zplus_le_reg_l with (p := (- m + Zmin n m)%Z).
- ring_simplify (- m + Zmin n m + m)%Z.
- ring_simplify (- m + Zmin n m + (n + m - Zmin n m))%Z.
- apply Zle_min_l.
+ apply Zplus_le_reg_l with (p := (- m + Z.min n m)%Z).
+ ring_simplify (- m + Z.min n m + m)%Z.
+ ring_simplify (- m + Z.min n m + (n + m - Z.min n m))%Z.
+ apply Z.le_min_l.
 Qed.
 
 
-Lemma Zmin_or_informative : forall n m : Z, {Zmin n m = n} + {Zmin n m = m}.
+Lemma Zmin_or_informative : forall n m : Z, {Z.min n m = n} + {Z.min n m = m}.
 Proof.
  intros.
  case (Z_lt_ge_dec n m).
- unfold Zmin in |- *.
- unfold Zlt in |- *.
+ unfold Z.min in |- *.
+ unfold Z.lt in |- *.
  intro z.
  rewrite z.
  left.
@@ -2880,8 +2880,8 @@ Proof.
  intro.
  case H.
  intros z0.
- unfold Zmin in |- *.
- unfold Zgt in z0.
+ unfold Z.min in |- *.
+ unfold Z.gt in z0.
  rewrite z0.
  right.
  reflexivity.
@@ -2894,14 +2894,14 @@ Proof.
  elim H.
  intro.
  left.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  intro.
  right.
  symmetry  in |- *.
  assumption.
- apply Z_le_lt_eq_dec. 
- apply Zge_le.
+ apply Z_le_lt_eq_dec.
+ apply Z.ge_le.
  assumption.
 Qed.
 
@@ -2925,8 +2925,8 @@ Proof.
  assumption.
  ring.
 Qed.
- 
-Lemma Zmax_or_informative : forall n m : Z, {Zmax n m = n} + {Zmax n m = m}. 
+
+Lemma Zmax_or_informative : forall n m : Z, {Zmax n m = n} + {Zmax n m = m}.
 Proof.
  intros.
  unfold Zmax in |- *.
@@ -2960,12 +2960,12 @@ Proof.
  exact Zeven.Zeven_Sn.
 Qed.
 
-Lemma Zeven_pred : forall x : Z, Zeven.Zodd x -> Zeven.Zeven (x - 1). 
+Lemma Zeven_pred : forall x : Z, Zeven.Zodd x -> Zeven.Zeven (x - 1).
 Proof.
  exact Zeven.Zeven_pred.
 Qed.
 
-(* This lemma used to be useful since it was mentioned with an unnecessary premise 
+(* This lemma used to be useful since it was mentioned with an unnecessary premise
    `x>=0` as Z_modulo_2 in ZArith, but the ZArith version has been fixed. *)
 
 Definition Z_modulo_2_always :
@@ -2987,10 +2987,10 @@ Proof.
 Qed.
 
 Lemma Z_div_le :
- forall a b c : Z, (0 < c)%Z -> (b <= a)%Z -> (b / c <= a / c)%Z. 
+ forall a b c : Z, (0 < c)%Z -> (b <= a)%Z -> (b / c <= a / c)%Z.
 Proof.
  intros.
- apply Zge_le.
+ apply Z.ge_le.
  apply Z_div_ge; Flip; assumption.
 Qed.
 
@@ -2998,7 +2998,7 @@ Lemma Z_div_nonneg :
  forall a b : Z, (0 < b)%Z -> (0 <= a)%Z -> (0 <= a / b)%Z.
 Proof.
  intros.
- apply Zge_le.
+ apply Z.ge_le.
  apply Z_div_ge0; Flip; assumption.
 Qed.
 
@@ -3012,7 +3012,7 @@ Proof.
  intro.
  apply (Zlt_not_le (b * (a / b) + a mod b) 0 H0).
  apply Zplus_le_0_compat.
- apply Zmult_le_0_compat. 
+ apply Zmult_le_0_compat.
  apply Zlt_le_weak; assumption.
  Flip.
  assumption.
diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v
index 445ffac8cb..fbe909ec41 100644
--- a/test-suite/success/Case11.v
+++ b/test-suite/success/Case11.v
@@ -5,9 +5,9 @@ Section A.
 
 Variables (Alpha : Set) (Beta : Set).
 
-Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) :
+Definition nodep_prod_of_dep (c : sigT (fun a : Alpha => Beta)) :
   Alpha * Beta := match c with
-                  | existS _ a b => (a, b)
+                  | existT _ a b => (a, b)
                   end.
 
 End A.
diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v
index 861d04668f..a4efcca945 100644
--- a/test-suite/success/Case17.v
+++ b/test-suite/success/Case17.v
@@ -1,5 +1,5 @@
 (* Check the synthesis of predicate from a cast in case of matching of
-   the first component (here [list bool]) of a dependent type (here [sigS])
+   the first component (here [list bool]) of a dependent type (here [sigT])
    (Simplification of an example from file parsing2.v of the Coq'Art
     exercises) *)
 
@@ -19,10 +19,10 @@ Axiom HHH : forall A : Prop, A.
 
 Check
   (match rec l0 (HHH _) with
-   | inleft (existS _ (false :: l1) _) => inright _ (HHH _)
-   | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
+   | inleft (existT _ (false :: l1) _) => inright _ (HHH _)
+   | inleft (existT _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
        inright _ (HHH _)
-   | inleft (existS _ _ _) => inright _ (HHH _)
+   | inleft (existT _ _ _) => inright _ (HHH _)
    | inright Hnp => inright _ (HHH _)
    end
    :{l'' : list bool &
@@ -39,10 +39,10 @@ Check
             {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
             {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) =>
    match rec l0 (HHH _) with
-   | inleft (existS _ (false :: l1) _) => inright _ (HHH _)
-   | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
+   | inleft (existT _ (false :: l1) _) => inright _ (HHH _)
+   | inleft (existT _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
        inright _ (HHH _)
-   | inleft (existS _ _ _) => inright _ (HHH _)
+   | inleft (existT _ _ _) => inright _ (HHH _)
    | inright Hnp => inright _ (HHH _)
    end
    :{l'' : list bool &
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 288c9d1da0..5650dba236 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq88.
+Import Coq.Compat.Coq89.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index b7bbc505b4..37d50ee67d 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq89.
 Import Coq.Compat.Coq88.
 Import Coq.Compat.Coq87.
-Import Coq.Compat.Coq86.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 9cfe60390f..9981388381 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq89.
 Import Coq.Compat.Coq88.
-Import Coq.Compat.Coq87.
diff --git a/test-suite/success/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v
deleted file mode 100644
index 8912197d2f..0000000000
--- a/test-suite/success/FunindExtraction_compat86.v
+++ /dev/null
@@ -1,506 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
-
-Definition iszero (n : nat) : bool :=
-  match n with
-  | O => true
-  | _ => false
-  end.
-
-Functional Scheme iszero_ind := Induction for iszero Sort Prop.
-
-Lemma toto : forall n : nat, n = 0 -> iszero n = true.
-intros x eg.
- functional induction iszero x; simpl.
-trivial.
-inversion eg.
-Qed.
-
-
-Function ftest (n m : nat) : nat :=
-  match n with
-  | O => match m with
-         | O => 0
-         | _ => 1
-         end
-  | S p => 0
-  end.
-(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *)
-
-Lemma test1 : forall n m : nat, ftest n m <= 2.
-intros n m.
- functional induction ftest n m; auto.
-Qed.
-
-Lemma test2 : forall m n, ~ 2 = ftest n m.
-Proof.
-intros n m;intro H.
-functional inversion H ftest.
-Qed.
-
-Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0)  \/ n <> 0.
-Proof.
-functional inversion 1 ftest;auto.
-Qed.
-
-
-Require Import Arith.
-Lemma test11 : forall m : nat, ftest 0 m <= 2.
-intros m.
- functional induction ftest 0 m.
-auto.
-auto.
-auto with *.
-Qed.
-
-Function lamfix (m n : nat) {struct n } : nat :=
-  match n with
-    | O => m
-    | S p => lamfix m p
-  end.
-
-(* Parameter v1 v2 : nat. *)
-
-Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1.
-intros v1 v2.
- functional induction lamfix v1 v2.
-trivial.
-assumption.
-Defined.
-
-
-
-(* polymorphic function *)
-Require Import List.
-
-Functional Scheme app_ind := Induction for app Sort Prop.
-
-Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
-intros A l l'.
- functional induction app A l l';  intuition.
- rewrite <- H0; trivial.
-Qed.
-
-
-
-
-
-Require Export Arith.
-
-
-Function trivfun (n : nat) : nat :=
-  match n with
-  | O => 0
-  | S m => trivfun m
-  end.
-
-
-(* essaie de parametre variables non locaux:*)
-
-Parameter varessai : nat.
-
-Lemma first_try : trivfun varessai = 0.
- functional induction trivfun varessai.
-trivial.
-assumption.
-Defined.
-
-
- Functional Scheme triv_ind := Induction for trivfun Sort Prop.
-
-Lemma bisrepetita : forall n' : nat, trivfun n' = 0.
-intros n'.
- functional induction trivfun n'.
-trivial.
-assumption.
-Qed.
-
-
-
-
-
-
-
-Function iseven (n : nat) : bool :=
-  match n with
-  | O => true
-  | S (S m) => iseven m
-  | _ => false
-  end.
-
-
-Function funex (n : nat) : nat :=
-  match iseven n with
-  | true => n
-  | false => match n with
-             | O => 0
-             | S r => funex r
-             end
-  end.
-
-
-Function nat_equal_bool (n m : nat) {struct n} : bool :=
-  match n with
-  | O => match m with
-         | O => true
-         | _ => false
-         end
-  | S p => match m with
-           | O => false
-           | S q => nat_equal_bool p q
-           end
-  end.
-
-
-Require Export Div2.
-Require Import Nat.
-Functional Scheme div2_ind := Induction for div2 Sort Prop.
-Lemma div2_inf : forall n : nat, div2 n <= n.
-intros n.
- functional induction div2 n.
-auto.
-auto.
-
-apply le_S.
-apply le_n_S.
-exact IHn0.
-Qed.
-
-(* reuse this lemma as a scheme:*)
-
-Function nested_lam (n : nat) : nat -> nat :=
-  match n with
-  | O => fun m : nat => 0
-  | S n' => fun m : nat => m + nested_lam n' m
-  end.
-
-
-Lemma nest : forall n m : nat, nested_lam n m = n * m.
-intros n m.
- functional induction nested_lam n m; simpl;auto.
-Qed.
-
-
-Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
-  let (n, m) := (p: nat*nat) in
-  match n with
-  | O => 0
-  | S q => match x with
-           | O => 1
-           | S r => S (essai r (q, m))
-           end
-  end.
-
-Lemma essai_essai :
- forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p.
-intros x p.
- functional induction essai x p; intros.
-inversion H.
-auto with arith.
- auto with arith.
-Qed.
-
-Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
-  let x := nat_equal_bool m 5 in
-  let y := 0 in
-  match n with
-  | O => y
-  | S q =>
-      let recapp := plus_x_not_five'' q m in
-      match x with
-      | true => S recapp
-      | false => S recapp
-      end
-  end.
-
-Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
-intros a b.
- functional induction plus_x_not_five'' a b; intros hyp; simpl; auto.
-Qed.
-
-Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
-intros n m.
- functional induction nat_equal_bool n m; simpl; intros hyp; auto.
-rewrite <- hyp in y; simpl in y;tauto.
-inversion hyp.
-Qed.
-
-Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
-intros n m.
- functional induction nat_equal_bool n m; simpl; intros eg; auto.
-inversion eg.
-inversion eg.
-Qed.
-
-
-Inductive istrue : bool -> Prop :=
-    istrue0 : istrue true.
-
-Functional Scheme add_ind := Induction for add Sort Prop.
-
-Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
-intros n m.
- functional induction add n m; intros.
-auto with arith.
-auto with arith.
-Qed.
-
-
-Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
-intros n.
-unfold plus.
- functional induction plus n 0; intros.
-auto with arith.
-apply le_n_S.
-assumption.
-Qed.
-
-Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x.
-intros n.
- functional induction plus 0 n; intros; auto with arith.
-Qed.
-
-Function mod2 (n : nat) : nat :=
-  match n with
-  | O => 0
-  | S (S m) => S (mod2 m)
-  | _ => 0
-  end.
-
-Lemma princ_mod2 : forall n : nat, mod2 n <= n.
-intros n.
- functional induction mod2 n; simpl; auto with arith.
-Qed.
-
-Function isfour (n : nat) : bool :=
-  match n with
-  | S (S (S (S O))) => true
-  | _ => false
-  end.
-
-Function isononeorfour (n : nat) : bool :=
-  match n with
-  | S O => true
-  | S (S (S (S O))) => true
-  | _ => false
-  end.
-
-Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
-intros n.
- functional induction isononeorfour n; intros istr; simpl;
- inversion istr.
-apply istrue0.
-destruct n. inversion istr.
-destruct n. tauto.
-destruct n. inversion istr.
-destruct n. inversion istr.
-destruct n. tauto.
-simpl in *. inversion H0.
-Qed.
-
-Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
-intros n.
- functional induction isononeorfour n; intros m istr; inversion istr.
-apply istrue0.
-rewrite H in y; simpl in y;tauto.
-Qed.
-
-Function ftest4 (n m : nat) : nat :=
-  match n with
-  | O => match m with
-         | O => 0
-         | S q => 1
-         end
-  | S p => match m with
-           | O => 0
-           | S r => 1
-           end
-  end.
-
-Lemma test4 : forall n m : nat, ftest n m <= 2.
-intros n m.
- functional induction ftest n m; auto with arith.
-Qed.
-
-Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
-intros n m.
-assert ({n0 | n0 = S n}).
-exists (S n);reflexivity.
-destruct H as [n0 H1].
-rewrite <- H1;revert H1.
- functional induction ftest4 n0 m.
-inversion 1.
-inversion 1.
-
-auto with arith.
-auto with arith.
-Qed.
-
-Function ftest44 (x : nat * nat) (n m : nat) : nat :=
-  let (p, q) := (x: nat*nat) in
-  match n with
-  | O => match m with
-         | O => 0
-         | S q => 1
-         end
-  | S p => match m with
-           | O => 0
-           | S r => 1
-           end
-  end.
-
-Lemma test44 :
- forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2.
-intros pq n m o r s.
- functional induction ftest44 pq n (S m).
-auto with arith.
-auto with arith.
-auto with arith.
-auto with arith.
-Qed.
-
-Function ftest2 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => match m with
-         | O => 0
-         | S q => 0
-         end
-  | S p => ftest2 p m
-  end.
-
-Lemma test2' : forall n m : nat, ftest2 n m <= 2.
-intros n m.
- functional induction ftest2 n m; simpl; intros; auto.
-Qed.
-
-Function ftest3 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => 0
-  | S p => match m with
-           | O => ftest3 p 0
-           | S r => 0
-           end
-  end.
-
-Lemma test3' : forall n m : nat, ftest3 n m <= 2.
-intros n m.
- functional induction ftest3 n m.
-intros.
-auto.
-intros.
-auto.
-intros.
-simpl.
-auto.
-Qed.
-
-Function ftest5 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => 0
-  | S p => match m with
-           | O => ftest5 p 0
-           | S r => ftest5 p r
-           end
-  end.
-
-Lemma test5 : forall n m : nat, ftest5 n m <= 2.
-intros n m.
- functional induction ftest5 n m.
-intros.
-auto.
-intros.
-auto.
-intros.
-simpl.
-auto.
-Qed.
-
-Function ftest7 (n : nat) : nat :=
-  match ftest5 n 0 with
-  | O => 0
-  | S r => 0
-  end.
-
-Lemma essai7 :
- forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2)
-   (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2)
-   (n : nat), ftest7 n <= 2.
-intros hyp1 hyp2 n.
- functional induction ftest7 n; auto.
-Qed.
-
-Function ftest6 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => 0
-  | S p => match ftest5 p 0 with
-           | O => ftest6 p 0
-           | S r => ftest6 p r
-           end
-  end.
-
-
-Lemma princ6 :
- (forall n m : nat, n = 0 -> ftest6 0 m <= 2) ->
- (forall n m p : nat,
-  ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) ->
- (forall n m p r : nat,
-  ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) ->
- forall x y : nat, ftest6 x y <= 2.
-intros hyp1 hyp2 hyp3 n m.
-generalize hyp1 hyp2 hyp3.
-clear hyp1 hyp2 hyp3.
- functional induction ftest6 n m; auto.
-Qed.
-
-Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
-intros n m.
- functional induction ftest6 n m; simpl; auto.
-Qed.
-
-(* Some tests with modules *)
-Module M.
-Function test_m (n:nat) : nat :=
-  match n with
-    | 0 => 0
-    | S n =>  S (S (test_m n))
-  end.
-
-Lemma test_m_is_double :  forall n, div2 (test_m n) = n.
-Proof.
-intros n.
-functional induction (test_m n).
-reflexivity.
-simpl;rewrite IHn0;reflexivity.
-Qed.
-End M.
-(* We redefine a new Function with the same name *)
-Function test_m (n:nat) : nat :=
-  pred n.
-
-Lemma test_m_is_pred : forall n, test_m n = pred n.
-Proof.
-intro n.
-functional induction (test_m n). (* the test_m_ind to use is the last defined  saying that test_m = pred*)
-reflexivity.
-Qed.
-
-(* Checks if the dot notation are correctly treated in infos *)
-Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n.
-intro n.
-(* here we should apply M.test_m_ind *)
-functional induction (M.test_m n).
-reflexivity.
-simpl;rewrite IHn0;reflexivity.
-Qed.
-
-Import M.
-(* Now test_m is the one which defines double *)
-
-Lemma test_m_is_double : forall n, div2 (M.test_m n) = n.
-intro n.
-(* here we should apply M.test_m_ind *)
-functional induction (test_m n).
-reflexivity.
-simpl;rewrite IHn0;reflexivity.
-Qed.
-
-Extraction iszero.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 78652fb64b..7ee471bae7 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -19,8 +19,8 @@ Qed.
 (* Check that no tuple needs to be built *)
 Lemma l3 :
  forall x y : nat,
- existS (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) =
- existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) ->
+ existT (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) =
+ existT (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) ->
  x = y.
 intros x y H.
  injection H.
@@ -30,10 +30,10 @@ Qed.
 (* Check that a tuple is built (actually the same as the initial one) *)
 Lemma l4 :
  forall p1 p2 : {0 = 0} + {0 = 0},
- existS (fun n : nat => {n = n} + {n = n}) 0 p1 =
- existS (fun n : nat => {n = n} + {n = n}) 0 p2 ->
- existS (fun n : nat => {n = n} + {n = n}) 0 p1 =
- existS (fun n : nat => {n = n} + {n = n}) 0 p2.
+ existT (fun n : nat => {n = n} + {n = n}) 0 p1 =
+ existT (fun n : nat => {n = n} + {n = n}) 0 p2 ->
+ existT (fun n : nat => {n = n} + {n = n}) 0 p1 =
+ existT (fun n : nat => {n = n} + {n = n}) 0 p2.
 intros.
  injection H.
 exact (fun H => H).
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 448d0082db..baf089796f 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -7,7 +7,7 @@ Inductive listn : nat -> Set :=
 Axiom
   ax :
     forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
-    existS _ (n + n') l = existS _ (n' + n) l'.
+    existT _ (n + n') l = existT _ (n' + n) l'.
 
 Lemma lem :
  forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
@@ -72,7 +72,7 @@ Qed.
 
 Require Import JMeq.
 
-Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True.  
+Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True.
 inversion 1; (* Goal is now [JMeq a a -> True] *) dependent rewrite H3.
 Undo.
 intros; inversion H; dependent rewrite H4 in H0.
@@ -135,7 +135,7 @@ Abort.
 Goal forall x y, x=y+0 -> let z := x+1 in x+1=y -> z=z -> z=x.
 intros.
 subst x. (* was failing *)
-subst z. 
+subst z.
 rewrite H0.
 auto with arith.
 Qed.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
new file mode 100755
index 0000000000..02a2348450
--- /dev/null
+++ b/test-suite/tools/update-compat/run.sh
@@ -0,0 +1,9 @@
+#!/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 --cur-version=8.9 || exit $?
diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 713aef858e..6f220f2023 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -135,10 +135,10 @@ Qed.
     See now [Nat.compare] and its properties.
     In scope [nat_scope], the notation for [Nat.compare] is "?=" *)
 
-Notation nat_compare := Nat.compare (compat "8.6").
+Notation nat_compare := Nat.compare (compat "8.7").
 
-Notation nat_compare_spec := Nat.compare_spec (compat "8.6").
-Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.6").
+Notation nat_compare_spec := Nat.compare_spec (compat "8.7").
+Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.7").
 Notation nat_compare_S := Nat.compare_succ (only parsing).
 
 Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt.
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 578425bfb5..950cd8242b 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
+Require Export Coq.Compat.Coq89.
+
 (** In Coq 8.9, prim token notations follow [Import] rather than
     [Require].  So we make all of the relevant notations accessible in
     compatibility mode. *)
diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq89.v
index 666be207eb..d25671887f 100644
--- a/theories/Compat/Coq86.v
+++ b/theories/Compat/Coq89.v
@@ -8,8 +8,4 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Compatibility file for making Coq act similar to Coq v8.6 *)
-Require Export Coq.Compat.Coq87.
-
-Require Export Coq.extraction.Extraction.
-Require Export Coq.funind.FunInd.
+(** Compatibility file for making Coq act similar to Coq v8.9 *)
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 997059669d..2d5a79838a 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -26,7 +26,7 @@ Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
-Notation option_map := option_map (compat "8.6").
+Notation option_map := option_map (compat "8.7").
 
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index d6a0fb214f..a5f926f7ab 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -782,16 +782,16 @@ Hint Resolve exist exist2 existT existT2: core.
 
 (* Compatibility *)
 
-Notation sigS := sigT (compat "8.6").
-Notation existS := existT (compat "8.6").
-Notation sigS_rect := sigT_rect (compat "8.6").
-Notation sigS_rec := sigT_rec (compat "8.6").
-Notation sigS_ind := sigT_ind (compat "8.6").
-Notation projS1 := projT1 (compat "8.6").
-Notation projS2 := projT2 (compat "8.6").
-
-Notation sigS2 := sigT2 (compat "8.6").
-Notation existS2 := existT2 (compat "8.6").
-Notation sigS2_rect := sigT2_rect (compat "8.6").
-Notation sigS2_rec := sigT2_rec (compat "8.6").
-Notation sigS2_ind := sigT2_ind (compat "8.6").
+Notation sigS := sigT (compat "8.7").
+Notation existS := existT (compat "8.7").
+Notation sigS_rect := sigT_rect (compat "8.7").
+Notation sigS_rec := sigT_rec (compat "8.7").
+Notation sigS_ind := sigT_ind (compat "8.7").
+Notation projS1 := projT1 (compat "8.7").
+Notation projS2 := projT2 (compat "8.7").
+
+Notation sigS2 := sigT2 (compat "8.7").
+Notation existS2 := existT2 (compat "8.7").
+Notation sigS2_rect := sigT2_rect (compat "8.7").
+Notation sigS2_rec := sigT2_rec (compat "8.7").
+Notation sigS2_ind := sigT2_ind (compat "8.7").
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index d938b315f1..8e59941f37 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -125,7 +125,7 @@ Proof.
   apply eq_dep_intro.
 Qed.
 
-Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.6"). (* Compatibility *)
+Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.7"). (* Compatibility *)
 
 Lemma eq_dep_eq_sigT :
   forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index bd27f94abd..92c124ec32 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -966,33 +966,33 @@ Notation N_ind := N_ind (only parsing).
 Notation N0 := N0 (only parsing).
 Notation Npos := N.pos (only parsing).
 
-Notation Ndiscr := N.discr (compat "8.6").
+Notation Ndiscr := N.discr (compat "8.7").
 Notation Ndouble_plus_one := N.succ_double (only parsing).
-Notation Ndouble := N.double (compat "8.6").
-Notation Nsucc := N.succ (compat "8.6").
-Notation Npred := N.pred (compat "8.6").
-Notation Nsucc_pos := N.succ_pos (compat "8.6").
-Notation Ppred_N := Pos.pred_N (compat "8.6").
+Notation Ndouble := N.double (compat "8.7").
+Notation Nsucc := N.succ (compat "8.7").
+Notation Npred := N.pred (compat "8.7").
+Notation Nsucc_pos := N.succ_pos (compat "8.7").
+Notation Ppred_N := Pos.pred_N (compat "8.7").
 Notation Nplus := N.add (only parsing).
 Notation Nminus := N.sub (only parsing).
 Notation Nmult := N.mul (only parsing).
-Notation Neqb := N.eqb (compat "8.6").
-Notation Ncompare := N.compare (compat "8.6").
-Notation Nlt := N.lt (compat "8.6").
-Notation Ngt := N.gt (compat "8.6").
-Notation Nle := N.le (compat "8.6").
-Notation Nge := N.ge (compat "8.6").
-Notation Nmin := N.min (compat "8.6").
-Notation Nmax := N.max (compat "8.6").
-Notation Ndiv2 := N.div2 (compat "8.6").
-Notation Neven := N.even (compat "8.6").
-Notation Nodd := N.odd (compat "8.6").
-Notation Npow := N.pow (compat "8.6").
-Notation Nlog2 := N.log2 (compat "8.6").
+Notation Neqb := N.eqb (compat "8.7").
+Notation Ncompare := N.compare (compat "8.7").
+Notation Nlt := N.lt (compat "8.7").
+Notation Ngt := N.gt (compat "8.7").
+Notation Nle := N.le (compat "8.7").
+Notation Nge := N.ge (compat "8.7").
+Notation Nmin := N.min (compat "8.7").
+Notation Nmax := N.max (compat "8.7").
+Notation Ndiv2 := N.div2 (compat "8.7").
+Notation Neven := N.even (compat "8.7").
+Notation Nodd := N.odd (compat "8.7").
+Notation Npow := N.pow (compat "8.7").
+Notation Nlog2 := N.log2 (compat "8.7").
 
 Notation nat_of_N := N.to_nat (only parsing).
 Notation N_of_nat := N.of_nat (only parsing).
-Notation N_eq_dec := N.eq_dec (compat "8.6").
+Notation N_eq_dec := N.eq_dec (compat "8.7").
 Notation Nrect := N.peano_rect (only parsing).
 Notation Nrect_base := N.peano_rect_base (only parsing).
 Notation Nrect_step := N.peano_rect_succ (only parsing).
@@ -1001,11 +1001,11 @@ Notation Nrec := N.peano_rec (only parsing).
 Notation Nrec_base := N.peano_rec_base (only parsing).
 Notation Nrec_succ := N.peano_rec_succ (only parsing).
 
-Notation Npred_succ := N.pred_succ (compat "8.6").
+Notation Npred_succ := N.pred_succ (compat "8.7").
 Notation Npred_minus := N.pred_sub (only parsing).
-Notation Nsucc_pred := N.succ_pred (compat "8.6").
+Notation Nsucc_pred := N.succ_pred (compat "8.7").
 Notation Ppred_N_spec := N.pos_pred_spec (only parsing).
-Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.6").
+Notation Nsucc_pos_spec := N.succ_pos_spec (compat "8.7").
 Notation Ppred_Nsucc := N.pos_pred_succ (only parsing).
 Notation Nplus_0_l := N.add_0_l (only parsing).
 Notation Nplus_0_r := N.add_0_r (only parsing).
@@ -1013,7 +1013,7 @@ Notation Nplus_comm := N.add_comm (only parsing).
 Notation Nplus_assoc := N.add_assoc (only parsing).
 Notation Nplus_succ := N.add_succ_l (only parsing).
 Notation Nsucc_0 := N.succ_0_discr (only parsing).
-Notation Nsucc_inj := N.succ_inj (compat "8.6").
+Notation Nsucc_inj := N.succ_inj (compat "8.7").
 Notation Nminus_N0_Nle := N.sub_0_le (only parsing).
 Notation Nminus_0_r := N.sub_0_r (only parsing).
 Notation Nminus_succ_r:= N.sub_succ_r (only parsing).
@@ -1023,29 +1023,29 @@ Notation Nmult_1_r := N.mul_1_r (only parsing).
 Notation Nmult_comm := N.mul_comm (only parsing).
 Notation Nmult_assoc := N.mul_assoc (only parsing).
 Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing).
-Notation Neqb_eq := N.eqb_eq (compat "8.6").
+Notation Neqb_eq := N.eqb_eq (compat "8.7").
 Notation Nle_0 := N.le_0_l (only parsing).
-Notation Ncompare_refl := N.compare_refl (compat "8.6").
+Notation Ncompare_refl := N.compare_refl (compat "8.7").
 Notation Ncompare_Eq_eq := N.compare_eq (only parsing).
 Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing).
-Notation Nlt_irrefl := N.lt_irrefl (compat "8.6").
-Notation Nlt_trans := N.lt_trans (compat "8.6").
+Notation Nlt_irrefl := N.lt_irrefl (compat "8.7").
+Notation Nlt_trans := N.lt_trans (compat "8.7").
 Notation Nle_lteq := N.lt_eq_cases (only parsing).
-Notation Nlt_succ_r := N.lt_succ_r (compat "8.6").
-Notation Nle_trans := N.le_trans (compat "8.6").
-Notation Nle_succ_l := N.le_succ_l (compat "8.6").
-Notation Ncompare_spec := N.compare_spec (compat "8.6").
+Notation Nlt_succ_r := N.lt_succ_r (compat "8.7").
+Notation Nle_trans := N.le_trans (compat "8.7").
+Notation Nle_succ_l := N.le_succ_l (compat "8.7").
+Notation Ncompare_spec := N.compare_spec (compat "8.7").
 Notation Ncompare_0 := N.compare_0_r (only parsing).
 Notation Ndouble_div2 := N.div2_double (only parsing).
 Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing).
-Notation Ndouble_inj := N.double_inj (compat "8.6").
+Notation Ndouble_inj := N.double_inj (compat "8.7").
 Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing).
-Notation Npow_0_r := N.pow_0_r (compat "8.6").
-Notation Npow_succ_r := N.pow_succ_r (compat "8.6").
-Notation Nlog2_spec := N.log2_spec (compat "8.6").
-Notation Nlog2_nonpos := N.log2_nonpos (compat "8.6").
-Notation Neven_spec := N.even_spec (compat "8.6").
-Notation Nodd_spec := N.odd_spec (compat "8.6").
+Notation Npow_0_r := N.pow_0_r (compat "8.7").
+Notation Npow_succ_r := N.pow_succ_r (compat "8.7").
+Notation Nlog2_spec := N.log2_spec (compat "8.7").
+Notation Nlog2_nonpos := N.log2_nonpos (compat "8.7").
+Notation Neven_spec := N.even_spec (compat "8.7").
+Notation Nodd_spec := N.odd_spec (compat "8.7").
 Notation Nlt_not_eq := N.lt_neq (only parsing).
 Notation Ngt_Nlt := N.gt_lt (only parsing).
 
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v
index 67c30f2250..e2b2b4904e 100644
--- a/theories/NArith/Ndec.v
+++ b/theories/NArith/Ndec.v
@@ -22,8 +22,8 @@ Local Open Scope N_scope.
 (** Obsolete results about boolean comparisons over [N],
     kept for compatibility with IntMap and SMC. *)
 
-Notation Peqb := Pos.eqb (compat "8.6").
-Notation Neqb := N.eqb (compat "8.6").
+Notation Peqb := Pos.eqb (compat "8.7").
+Notation Neqb := N.eqb (compat "8.7").
 Notation Peqb_correct := Pos.eqb_refl (only parsing).
 Notation Neqb_correct := N.eqb_refl (only parsing).
 Notation Neqb_comm := N.eqb_sym (only parsing).
diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v
index 7c9fd86958..885c0d48b1 100644
--- a/theories/NArith/Ndiv_def.v
+++ b/theories/NArith/Ndiv_def.v
@@ -24,10 +24,10 @@ Lemma Pdiv_eucl_remainder a b :
   snd (Pdiv_eucl a b) < Npos b.
 Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed.
 
-Notation Ndiv_eucl := N.div_eucl (compat "8.6").
-Notation Ndiv := N.div (compat "8.6").
+Notation Ndiv_eucl := N.div_eucl (compat "8.7").
+Notation Ndiv := N.div (compat "8.7").
 Notation Nmod := N.modulo (only parsing).
 
 Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing).
 Notation Ndiv_mod_eq := N.div_mod' (only parsing).
-Notation Nmod_lt := N.mod_lt (compat "8.6").
+Notation Nmod_lt := N.mod_lt (compat "8.7").
diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v
index e771fe9167..f043328375 100644
--- a/theories/NArith/Nsqrt_def.v
+++ b/theories/NArith/Nsqrt_def.v
@@ -13,8 +13,8 @@ Require Import BinNat.
 (** Obsolete file, see [BinNat] now,
     only compatibility notations remain here. *)
 
-Notation Nsqrtrem := N.sqrtrem (compat "8.6").
-Notation Nsqrt := N.sqrt (compat "8.6").
-Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.6").
+Notation Nsqrtrem := N.sqrtrem (compat "8.7").
+Notation Nsqrt := N.sqrt (compat "8.7").
+Notation Nsqrtrem_spec := N.sqrtrem_spec (compat "8.7").
 Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing).
-Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.6").
+Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (compat "8.7").
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index dcaae1606d..01ecdd710c 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -1907,12 +1907,12 @@ Notation IsNul := Pos.IsNul (only parsing).
 Notation IsPos := Pos.IsPos (only parsing).
 Notation IsNeg := Pos.IsNeg (only parsing).
 
-Notation Psucc := Pos.succ (compat "8.6").
+Notation Psucc := Pos.succ (compat "8.7").
 Notation Pplus := Pos.add (only parsing).
 Notation Pplus_carry := Pos.add_carry (only parsing).
-Notation Ppred := Pos.pred (compat "8.6").
-Notation Piter_op := Pos.iter_op (compat "8.6").
-Notation Piter_op_succ := Pos.iter_op_succ (compat "8.6").
+Notation Ppred := Pos.pred (compat "8.7").
+Notation Piter_op := Pos.iter_op (compat "8.7").
+Notation Piter_op_succ := Pos.iter_op_succ (compat "8.7").
 Notation Pmult_nat := (Pos.iter_op plus) (only parsing).
 Notation nat_of_P := Pos.to_nat (only parsing).
 Notation P_of_succ_nat := Pos.of_succ_nat (only parsing).
@@ -1922,29 +1922,29 @@ Notation positive_mask_rect := Pos.mask_rect (only parsing).
 Notation positive_mask_ind := Pos.mask_ind (only parsing).
 Notation positive_mask_rec := Pos.mask_rec (only parsing).
 Notation Pdouble_plus_one_mask := Pos.succ_double_mask (only parsing).
-Notation Pdouble_mask := Pos.double_mask (compat "8.6").
+Notation Pdouble_mask := Pos.double_mask (compat "8.7").
 Notation Pdouble_minus_two := Pos.double_pred_mask (only parsing).
 Notation Pminus_mask := Pos.sub_mask (only parsing).
 Notation Pminus_mask_carry := Pos.sub_mask_carry (only parsing).
 Notation Pminus := Pos.sub (only parsing).
 Notation Pmult := Pos.mul (only parsing).
 Notation iter_pos := @Pos.iter (only parsing).
-Notation Ppow := Pos.pow (compat "8.6").
-Notation Pdiv2 := Pos.div2 (compat "8.6").
-Notation Pdiv2_up := Pos.div2_up (compat "8.6").
+Notation Ppow := Pos.pow (compat "8.7").
+Notation Pdiv2 := Pos.div2 (compat "8.7").
+Notation Pdiv2_up := Pos.div2_up (compat "8.7").
 Notation Psize := Pos.size_nat (only parsing).
 Notation Psize_pos := Pos.size (only parsing).
 Notation Pcompare x y m := (Pos.compare_cont m x y) (only parsing).
-Notation Plt := Pos.lt (compat "8.6").
-Notation Pgt := Pos.gt (compat "8.6").
-Notation Ple := Pos.le (compat "8.6").
-Notation Pge := Pos.ge (compat "8.6").
-Notation Pmin := Pos.min (compat "8.6").
-Notation Pmax := Pos.max (compat "8.6").
-Notation Peqb := Pos.eqb (compat "8.6").
+Notation Plt := Pos.lt (compat "8.7").
+Notation Pgt := Pos.gt (compat "8.7").
+Notation Ple := Pos.le (compat "8.7").
+Notation Pge := Pos.ge (compat "8.7").
+Notation Pmin := Pos.min (compat "8.7").
+Notation Pmax := Pos.max (compat "8.7").
+Notation Peqb := Pos.eqb (compat "8.7").
 Notation positive_eq_dec := Pos.eq_dec (only parsing).
 Notation xI_succ_xO := Pos.xI_succ_xO (only parsing).
-Notation Psucc_discr := Pos.succ_discr (compat "8.6").
+Notation Psucc_discr := Pos.succ_discr (compat "8.7").
 Notation Psucc_o_double_minus_one_eq_xO :=
  Pos.succ_pred_double (only parsing).
 Notation Pdouble_minus_one_o_succ_eq_xI :=
@@ -1953,9 +1953,9 @@ Notation xO_succ_permute := Pos.double_succ (only parsing).
 Notation double_moins_un_xO_discr :=
  Pos.pred_double_xO_discr (only parsing).
 Notation Psucc_not_one := Pos.succ_not_1 (only parsing).
-Notation Ppred_succ := Pos.pred_succ (compat "8.6").
+Notation Ppred_succ := Pos.pred_succ (compat "8.7").
 Notation Psucc_pred := Pos.succ_pred_or (only parsing).
-Notation Psucc_inj := Pos.succ_inj (compat "8.6").
+Notation Psucc_inj := Pos.succ_inj (compat "8.7").
 Notation Pplus_carry_spec := Pos.add_carry_spec (only parsing).
 Notation Pplus_comm := Pos.add_comm (only parsing).
 Notation Pplus_succ_permute_r := Pos.add_succ_r (only parsing).
@@ -2002,17 +2002,17 @@ Notation Pmult_xO_discr := Pos.mul_xO_discr (only parsing).
 Notation Pmult_reg_r := Pos.mul_reg_r (only parsing).
 Notation Pmult_reg_l := Pos.mul_reg_l (only parsing).
 Notation Pmult_1_inversion_l := Pos.mul_eq_1_l (only parsing).
-Notation Psquare_xO := Pos.square_xO (compat "8.6").
-Notation Psquare_xI := Pos.square_xI (compat "8.6").
+Notation Psquare_xO := Pos.square_xO (compat "8.7").
+Notation Psquare_xI := Pos.square_xI (compat "8.7").
 Notation iter_pos_swap_gen := Pos.iter_swap_gen (only parsing).
 Notation iter_pos_swap := Pos.iter_swap (only parsing).
 Notation iter_pos_succ := Pos.iter_succ (only parsing).
 Notation iter_pos_plus := Pos.iter_add (only parsing).
 Notation iter_pos_invariant := Pos.iter_invariant (only parsing).
-Notation Ppow_1_r := Pos.pow_1_r (compat "8.6").
-Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.6").
-Notation Peqb_refl := Pos.eqb_refl (compat "8.6").
-Notation Peqb_eq := Pos.eqb_eq (compat "8.6").
+Notation Ppow_1_r := Pos.pow_1_r (compat "8.7").
+Notation Ppow_succ_r := Pos.pow_succ_r (compat "8.7").
+Notation Peqb_refl := Pos.eqb_refl (compat "8.7").
+Notation Peqb_eq := Pos.eqb_eq (compat "8.7").
 Notation Pcompare_refl_id := Pos.compare_cont_refl (only parsing).
 Notation Pcompare_eq_iff := Pos.compare_eq_iff (only parsing).
 Notation Pcompare_Gt_Lt := Pos.compare_cont_Gt_Lt (only parsing).
@@ -2022,23 +2022,23 @@ Notation Pcompare_Lt_Gt := Pos.compare_cont_Lt_Gt (only parsing).
 Notation Pcompare_antisym := Pos.compare_cont_antisym (only parsing).
 Notation ZC1 := Pos.gt_lt (only parsing).
 Notation ZC2 := Pos.lt_gt (only parsing).
-Notation Pcompare_spec := Pos.compare_spec (compat "8.6").
+Notation Pcompare_spec := Pos.compare_spec (compat "8.7").
 Notation Pcompare_p_Sp := Pos.lt_succ_diag_r (only parsing).
-Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.6").
+Notation Pcompare_succ_succ := Pos.compare_succ_succ (compat "8.7").
 Notation Pcompare_1 := Pos.nlt_1_r (only parsing).
 Notation Plt_1 := Pos.nlt_1_r (only parsing).
-Notation Plt_1_succ := Pos.lt_1_succ (compat "8.6").
-Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.6").
-Notation Plt_irrefl := Pos.lt_irrefl (compat "8.6").
-Notation Plt_trans := Pos.lt_trans (compat "8.6").
-Notation Plt_ind := Pos.lt_ind (compat "8.6").
-Notation Ple_lteq := Pos.le_lteq (compat "8.6").
-Notation Ple_refl := Pos.le_refl (compat "8.6").
-Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.6").
-Notation Plt_le_trans := Pos.lt_le_trans (compat "8.6").
-Notation Ple_trans := Pos.le_trans (compat "8.6").
-Notation Plt_succ_r := Pos.lt_succ_r (compat "8.6").
-Notation Ple_succ_l := Pos.le_succ_l (compat "8.6").
+Notation Plt_1_succ := Pos.lt_1_succ (compat "8.7").
+Notation Plt_lt_succ := Pos.lt_lt_succ (compat "8.7").
+Notation Plt_irrefl := Pos.lt_irrefl (compat "8.7").
+Notation Plt_trans := Pos.lt_trans (compat "8.7").
+Notation Plt_ind := Pos.lt_ind (compat "8.7").
+Notation Ple_lteq := Pos.le_lteq (compat "8.7").
+Notation Ple_refl := Pos.le_refl (compat "8.7").
+Notation Ple_lt_trans := Pos.le_lt_trans (compat "8.7").
+Notation Plt_le_trans := Pos.lt_le_trans (compat "8.7").
+Notation Ple_trans := Pos.le_trans (compat "8.7").
+Notation Plt_succ_r := Pos.lt_succ_r (compat "8.7").
+Notation Ple_succ_l := Pos.le_succ_l (compat "8.7").
 Notation Pplus_compare_mono_l := Pos.add_compare_mono_l (only parsing).
 Notation Pplus_compare_mono_r := Pos.add_compare_mono_r (only parsing).
 Notation Pplus_lt_mono_l := Pos.add_lt_mono_l (only parsing).
@@ -2057,8 +2057,8 @@ Notation Pmult_le_mono_r := Pos.mul_le_mono_r (only parsing).
 Notation Pmult_le_mono := Pos.mul_le_mono (only parsing).
 Notation Plt_plus_r := Pos.lt_add_r (only parsing).
 Notation Plt_not_plus_l := Pos.lt_not_add_l (only parsing).
-Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.6").
-Notation Ppred_mask := Pos.pred_mask (compat "8.6").
+Notation Ppow_gt_1 := Pos.pow_gt_1 (compat "8.7").
+Notation Ppred_mask := Pos.pred_mask (compat "8.7").
 Notation Pminus_mask_succ_r := Pos.sub_mask_succ_r (only parsing).
 Notation Pminus_mask_carry_spec := Pos.sub_mask_carry_spec (only parsing).
 Notation Pminus_succ_r := Pos.sub_succ_r (only parsing).
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index a11d491a8b..1241345338 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1571,40 +1571,40 @@ End Z2Pos.
 
 Notation Zdouble_plus_one := Z.succ_double (only parsing).
 Notation Zdouble_minus_one := Z.pred_double (only parsing).
-Notation Zdouble := Z.double (compat "8.6").
+Notation Zdouble := Z.double (compat "8.7").
 Notation ZPminus := Z.pos_sub (only parsing).
-Notation Zsucc' := Z.succ (compat "8.6").
-Notation Zpred' := Z.pred (compat "8.6").
-Notation Zplus' := Z.add (compat "8.6").
+Notation Zsucc' := Z.succ (compat "8.7").
+Notation Zpred' := Z.pred (compat "8.7").
+Notation Zplus' := Z.add (compat "8.7").
 Notation Zplus := Z.add (only parsing). (* Slightly incompatible *)
-Notation Zopp := Z.opp (compat "8.6").
-Notation Zsucc := Z.succ (compat "8.6").
-Notation Zpred := Z.pred (compat "8.6").
+Notation Zopp := Z.opp (compat "8.7").
+Notation Zsucc := Z.succ (compat "8.7").
+Notation Zpred := Z.pred (compat "8.7").
 Notation Zminus := Z.sub (only parsing).
 Notation Zmult := Z.mul (only parsing).
-Notation Zcompare := Z.compare (compat "8.6").
-Notation Zsgn := Z.sgn (compat "8.6").
-Notation Zle := Z.le (compat "8.6").
-Notation Zge := Z.ge (compat "8.6").
-Notation Zlt := Z.lt (compat "8.6").
-Notation Zgt := Z.gt (compat "8.6").
-Notation Zmax := Z.max (compat "8.6").
-Notation Zmin := Z.min (compat "8.6").
-Notation Zabs := Z.abs (compat "8.6").
-Notation Zabs_nat := Z.abs_nat (compat "8.6").
-Notation Zabs_N := Z.abs_N (compat "8.6").
+Notation Zcompare := Z.compare (compat "8.7").
+Notation Zsgn := Z.sgn (compat "8.7").
+Notation Zle := Z.le (compat "8.7").
+Notation Zge := Z.ge (compat "8.7").
+Notation Zlt := Z.lt (compat "8.7").
+Notation Zgt := Z.gt (compat "8.7").
+Notation Zmax := Z.max (compat "8.7").
+Notation Zmin := Z.min (compat "8.7").
+Notation Zabs := Z.abs (compat "8.7").
+Notation Zabs_nat := Z.abs_nat (compat "8.7").
+Notation Zabs_N := Z.abs_N (compat "8.7").
 Notation Z_of_nat := Z.of_nat (only parsing).
 Notation Z_of_N := Z.of_N (only parsing).
 
 Notation Zind := Z.peano_ind (only parsing).
-Notation Zopp_0 := Z.opp_0 (compat "8.6").
-Notation Zopp_involutive := Z.opp_involutive (compat "8.6").
-Notation Zopp_inj := Z.opp_inj (compat "8.6").
+Notation Zopp_0 := Z.opp_0 (compat "8.7").
+Notation Zopp_involutive := Z.opp_involutive (compat "8.7").
+Notation Zopp_inj := Z.opp_inj (compat "8.7").
 Notation Zplus_0_l := Z.add_0_l (only parsing).
 Notation Zplus_0_r := Z.add_0_r (only parsing).
 Notation Zplus_comm := Z.add_comm (only parsing).
 Notation Zopp_plus_distr := Z.opp_add_distr (only parsing).
-Notation Zopp_succ := Z.opp_succ (compat "8.6").
+Notation Zopp_succ := Z.opp_succ (compat "8.7").
 Notation Zplus_opp_r := Z.add_opp_diag_r (only parsing).
 Notation Zplus_opp_l := Z.add_opp_diag_l (only parsing).
 Notation Zplus_assoc := Z.add_assoc (only parsing).
@@ -1613,11 +1613,11 @@ Notation Zplus_reg_l := Z.add_reg_l (only parsing).
 Notation Zplus_succ_l := Z.add_succ_l (only parsing).
 Notation Zplus_succ_comm := Z.add_succ_comm (only parsing).
 Notation Zsucc_discr := Z.neq_succ_diag_r (only parsing).
-Notation Zsucc_inj := Z.succ_inj (compat "8.6").
-Notation Zsucc'_inj := Z.succ_inj (compat "8.6").
-Notation Zsucc'_pred' := Z.succ_pred (compat "8.6").
-Notation Zpred'_succ' := Z.pred_succ (compat "8.6").
-Notation Zpred'_inj := Z.pred_inj (compat "8.6").
+Notation Zsucc_inj := Z.succ_inj (compat "8.7").
+Notation Zsucc'_inj := Z.succ_inj (compat "8.7").
+Notation Zsucc'_pred' := Z.succ_pred (compat "8.7").
+Notation Zpred'_succ' := Z.pred_succ (compat "8.7").
+Notation Zpred'_inj := Z.pred_inj (compat "8.7").
 Notation Zsucc'_discr := Z.neq_succ_diag_r (only parsing).
 Notation Zminus_0_r := Z.sub_0_r (only parsing).
 Notation Zminus_diag := Z.sub_diag (only parsing).
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 9bcdb73afa..6cadf30f85 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -34,7 +34,7 @@ Lemma Zcompare_rec (P:Set) (n m:Z) :
   ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
 Proof. apply Zcompare_rect. Defined.
 
-Notation Z_eq_dec := Z.eq_dec (compat "8.6").
+Notation Z_eq_dec := Z.eq_dec (compat "8.7").
 
 Section decidability.
 
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 0d8450e36b..057eb49965 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -29,17 +29,17 @@ Local Open Scope Z_scope.
 (**********************************************************************)
 (** * Properties of absolute value *)
 
-Notation Zabs_eq := Z.abs_eq (compat "8.6").
+Notation Zabs_eq := Z.abs_eq (compat "8.7").
 Notation Zabs_non_eq := Z.abs_neq (only parsing).
 Notation Zabs_Zopp := Z.abs_opp (only parsing).
 Notation Zabs_pos := Z.abs_nonneg (only parsing).
-Notation Zabs_involutive := Z.abs_involutive (compat "8.6").
+Notation Zabs_involutive := Z.abs_involutive (compat "8.7").
 Notation Zabs_eq_case := Z.abs_eq_cases (only parsing).
-Notation Zabs_triangle := Z.abs_triangle (compat "8.6").
+Notation Zabs_triangle := Z.abs_triangle (compat "8.7").
 Notation Zsgn_Zabs := Z.sgn_abs (only parsing).
 Notation Zabs_Zsgn := Z.abs_sgn (only parsing).
 Notation Zabs_Zmult := Z.abs_mul (only parsing).
-Notation Zabs_square := Z.abs_square (compat "8.6").
+Notation Zabs_square := Z.abs_square (compat "8.7").
 
 (** * Proving a property of the absolute value by cases *)
 
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index c8432e27bb..6ccb0153de 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -183,15 +183,15 @@ Qed.
 
 (** Compatibility notations *)
 
-Notation Zcompare_refl := Z.compare_refl (compat "8.6").
+Notation Zcompare_refl := Z.compare_refl (compat "8.7").
 Notation Zcompare_Eq_eq := Z.compare_eq (only parsing).
 Notation Zcompare_Eq_iff_eq := Z.compare_eq_iff (only parsing).
-Notation Zcompare_spec := Z.compare_spec (compat "8.6").
-Notation Zmin_l := Z.min_l (compat "8.6").
-Notation Zmin_r := Z.min_r (compat "8.6").
-Notation Zmax_l := Z.max_l (compat "8.6").
-Notation Zmax_r := Z.max_r (compat "8.6").
-Notation Zabs_eq := Z.abs_eq (compat "8.6").
+Notation Zcompare_spec := Z.compare_spec (compat "8.7").
+Notation Zmin_l := Z.min_l (compat "8.7").
+Notation Zmin_r := Z.min_r (compat "8.7").
+Notation Zmax_l := Z.max_l (compat "8.7").
+Notation Zmax_r := Z.max_r (compat "8.7").
+Notation Zabs_eq := Z.abs_eq (compat "8.7").
 Notation Zabs_non_eq := Z.abs_neq (only parsing).
 Notation Zsgn_0 := Z.sgn_null (only parsing).
 Notation Zsgn_1 := Z.sgn_pos (only parsing).
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 15d0e48747..74614e114a 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -21,11 +21,11 @@ Local Open Scope Z_scope.
     specifications and properties are in [BinInt]. *)
 
 Notation Zdiv_eucl_POS := Z.pos_div_eucl (only parsing).
-Notation Zdiv_eucl := Z.div_eucl (compat "8.6").
-Notation Zdiv := Z.div (compat "8.6").
+Notation Zdiv_eucl := Z.div_eucl (compat "8.7").
+Notation Zdiv := Z.div (compat "8.7").
 Notation Zmod := Z.modulo (only parsing).
 
-Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.6").
+Notation Zdiv_eucl_eq := Z.div_eucl_eq (compat "8.7").
 Notation Z_div_mod_eq_full := Z.div_mod (only parsing).
 Notation Zmod_POS_bound := Z.pos_div_eucl_bound (only parsing).
 Notation Zmod_pos_bound := Z.mod_pos_bound (only parsing).
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 00a58b517e..9e83bfc136 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -141,8 +141,8 @@ Notation Zodd_bool_pred := Z.odd_pred (only parsing).
 (** * Definition of [Z.quot2], [Z.div2] and properties wrt [Zeven]
   and [Zodd] *)
 
-Notation Zdiv2 := Z.div2 (compat "8.6").
-Notation Zquot2 := Z.quot2 (compat "8.6").
+Notation Zdiv2 := Z.div2 (compat "8.7").
+Notation Zquot2 := Z.quot2 (compat "8.7").
 
 (** Properties of [Z.div2] *)
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 7f595fcfd0..26bd9e8171 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -18,22 +18,22 @@ Local Open Scope Z_scope.
 
 (** Exact compatibility *)
 
-Notation Zmax_case := Z.max_case (compat "8.6").
-Notation Zmax_case_strong := Z.max_case_strong (compat "8.6").
+Notation Zmax_case := Z.max_case (compat "8.7").
+Notation Zmax_case_strong := Z.max_case_strong (compat "8.7").
 Notation Zmax_right := Z.max_r (only parsing).
-Notation Zle_max_l := Z.le_max_l (compat "8.6").
-Notation Zle_max_r := Z.le_max_r (compat "8.6").
-Notation Zmax_lub := Z.max_lub (compat "8.6").
-Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.6").
+Notation Zle_max_l := Z.le_max_l (compat "8.7").
+Notation Zle_max_r := Z.le_max_r (compat "8.7").
+Notation Zmax_lub := Z.max_lub (compat "8.7").
+Notation Zmax_lub_lt := Z.max_lub_lt (compat "8.7").
 Notation Zle_max_compat_r := Z.max_le_compat_r (only parsing).
 Notation Zle_max_compat_l := Z.max_le_compat_l (only parsing).
 Notation Zmax_idempotent := Z.max_id (only parsing).
 Notation Zmax_n_n := Z.max_id (only parsing).
-Notation Zmax_comm := Z.max_comm (compat "8.6").
-Notation Zmax_assoc := Z.max_assoc (compat "8.6").
+Notation Zmax_comm := Z.max_comm (compat "8.7").
+Notation Zmax_assoc := Z.max_assoc (compat "8.7").
 Notation Zmax_irreducible_dec := Z.max_dec (only parsing).
 Notation Zmax_le_prime := Z.max_le (only parsing).
-Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.6").
+Notation Zsucc_max_distr := Z.succ_max_distr (compat "8.7").
 Notation Zmax_SS := Z.succ_max_distr (only parsing).
 Notation Zplus_max_distr_l := Z.add_max_distr_l (only parsing).
 Notation Zplus_max_distr_r := Z.add_max_distr_r (only parsing).
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 6bc72227b2..5509ee7865 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -18,20 +18,20 @@ Local Open Scope Z_scope.
 
 (** Exact compatibility *)
 
-Notation Zmin_case := Z.min_case (compat "8.6").
-Notation Zmin_case_strong := Z.min_case_strong (compat "8.6").
-Notation Zle_min_l := Z.le_min_l (compat "8.6").
-Notation Zle_min_r := Z.le_min_r (compat "8.6").
-Notation Zmin_glb := Z.min_glb (compat "8.6").
-Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.6").
+Notation Zmin_case := Z.min_case (compat "8.7").
+Notation Zmin_case_strong := Z.min_case_strong (compat "8.7").
+Notation Zle_min_l := Z.le_min_l (compat "8.7").
+Notation Zle_min_r := Z.le_min_r (compat "8.7").
+Notation Zmin_glb := Z.min_glb (compat "8.7").
+Notation Zmin_glb_lt := Z.min_glb_lt (compat "8.7").
 Notation Zle_min_compat_r := Z.min_le_compat_r (only parsing).
 Notation Zle_min_compat_l := Z.min_le_compat_l (only parsing).
 Notation Zmin_idempotent := Z.min_id (only parsing).
 Notation Zmin_n_n := Z.min_id (only parsing).
-Notation Zmin_comm := Z.min_comm (compat "8.6").
-Notation Zmin_assoc := Z.min_assoc (compat "8.6").
+Notation Zmin_comm := Z.min_comm (compat "8.7").
+Notation Zmin_assoc := Z.min_assoc (compat "8.7").
 Notation Zmin_irreducible_inf := Z.min_dec (only parsing).
-Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.6").
+Notation Zsucc_min_distr := Z.succ_min_distr (compat "8.7").
 Notation Zmin_SS := Z.succ_min_distr (only parsing).
 Notation Zplus_min_distr_r := Z.add_min_distr_r (only parsing).
 Notation Zmin_plus := Z.add_min_distr_r (only parsing).
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index f5444c31d7..e6066d53f9 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -27,20 +27,20 @@ Open Scope Z_scope.
      - properties of the efficient [Z.gcd] function
 *)
 
-Notation Zgcd := Z.gcd (compat "8.6").
-Notation Zggcd := Z.ggcd (compat "8.6").
-Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.6").
-Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.6").
-Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.6").
-Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.6").
-Notation Zgcd_greatest := Z.gcd_greatest (compat "8.6").
-Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.6").
-Notation Zggcd_opp := Z.ggcd_opp (compat "8.6").
+Notation Zgcd := Z.gcd (compat "8.7").
+Notation Zggcd := Z.ggcd (compat "8.7").
+Notation Zggcd_gcd := Z.ggcd_gcd (compat "8.7").
+Notation Zggcd_correct_divisors := Z.ggcd_correct_divisors (compat "8.7").
+Notation Zgcd_divide_l := Z.gcd_divide_l (compat "8.7").
+Notation Zgcd_divide_r := Z.gcd_divide_r (compat "8.7").
+Notation Zgcd_greatest := Z.gcd_greatest (compat "8.7").
+Notation Zgcd_nonneg := Z.gcd_nonneg (compat "8.7").
+Notation Zggcd_opp := Z.ggcd_opp (compat "8.7").
 
 (** The former specialized inductive predicate [Z.divide] is now
     a generic existential predicate. *)
 
-Notation Zdivide := Z.divide (compat "8.6").
+Notation Zdivide := Z.divide (compat "8.7").
 
 (** Its former constructor is now a pseudo-constructor. *)
 
@@ -48,7 +48,7 @@ Definition Zdivide_intro a b q (H:b=q*a) : Z.divide a b := ex_intro _ q H.
 
 (** Results concerning divisibility*)
 
-Notation Zdivide_refl := Z.divide_refl (compat "8.6").
+Notation Zdivide_refl := Z.divide_refl (compat "8.7").
 Notation Zone_divide := Z.divide_1_l (only parsing).
 Notation Zdivide_0 := Z.divide_0_r (only parsing).
 Notation Zmult_divide_compat_l := Z.mul_divide_mono_l (only parsing).
@@ -97,8 +97,8 @@ Notation Zdivide_1 := Z.divide_1_r (only parsing).
 
 (** If [a] divides [b] and [b] divides [a] then [a] is [b] or [-b]. *)
 
-Notation Zdivide_antisym := Z.divide_antisym (compat "8.6").
-Notation Zdivide_trans := Z.divide_trans (compat "8.6").
+Notation Zdivide_antisym := Z.divide_antisym (compat "8.7").
+Notation Zdivide_trans := Z.divide_trans (compat "8.7").
 
 (** If [a] divides [b] and [b<>0] then [|a| <= |b|]. *)
 
@@ -800,7 +800,7 @@ Proof.
   rewrite <- Zdivide_Zdiv_eq; auto.
 Qed.
 
-Notation Zgcd_comm := Z.gcd_comm (compat "8.6").
+Notation Zgcd_comm := Z.gcd_comm (compat "8.7").
 
 Lemma Zgcd_ass a b c : Z.gcd (Z.gcd a b) c = Z.gcd a (Z.gcd b c).
 Proof.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index a1ec4b35e0..208e84aeb7 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -66,10 +66,10 @@ Qed.
 
 (** * Relating strict and large orders *)
 
-Notation Zgt_lt := Z.gt_lt (compat "8.6").
-Notation Zlt_gt := Z.lt_gt (compat "8.6").
-Notation Zge_le := Z.ge_le (compat "8.6").
-Notation Zle_ge := Z.le_ge (compat "8.6").
+Notation Zgt_lt := Z.gt_lt (compat "8.7").
+Notation Zlt_gt := Z.lt_gt (compat "8.7").
+Notation Zge_le := Z.ge_le (compat "8.7").
+Notation Zle_ge := Z.le_ge (compat "8.7").
 Notation Zgt_iff_lt := Z.gt_lt_iff (only parsing).
 Notation Zge_iff_le := Z.ge_le_iff (only parsing).
 
@@ -123,7 +123,7 @@ Qed.
 
 (** Reflexivity *)
 
-Notation Zle_refl := Z.le_refl (compat "8.6").
+Notation Zle_refl := Z.le_refl (compat "8.7").
 Notation Zeq_le := Z.eq_le_incl (only parsing).
 
 Hint Resolve Z.le_refl: zarith.
@@ -143,7 +143,7 @@ Qed.
 
 (** Irreflexivity *)
 
-Notation Zlt_irrefl := Z.lt_irrefl (compat "8.6").
+Notation Zlt_irrefl := Z.lt_irrefl (compat "8.7").
 Notation Zlt_not_eq := Z.lt_neq (only parsing).
 
 Lemma Zgt_irrefl n : ~ n > n.
@@ -167,7 +167,7 @@ Notation Zle_or_lt := Z.le_gt_cases (only parsing).
 
 (** Transitivity of strict orders *)
 
-Notation Zlt_trans := Z.lt_trans (compat "8.6").
+Notation Zlt_trans := Z.lt_trans (compat "8.7").
 
 Lemma Zgt_trans n m p : n > m -> m > p -> n > p.
 Proof.
@@ -176,8 +176,8 @@ Qed.
 
 (** Mixed transitivity *)
 
-Notation Zlt_le_trans := Z.lt_le_trans (compat "8.6").
-Notation Zle_lt_trans := Z.le_lt_trans (compat "8.6").
+Notation Zlt_le_trans := Z.lt_le_trans (compat "8.7").
+Notation Zle_lt_trans := Z.le_lt_trans (compat "8.7").
 
 Lemma Zle_gt_trans n m p : m <= n -> m > p -> n > p.
 Proof.
@@ -191,7 +191,7 @@ Qed.
 
 (** Transitivity of large orders *)
 
-Notation Zle_trans := Z.le_trans (compat "8.6").
+Notation Zle_trans := Z.le_trans (compat "8.7").
 
 Lemma Zge_trans n m p : n >= m -> m >= p -> n >= p.
 Proof.
@@ -257,8 +257,8 @@ Qed.
 
 (** Relating strict and large order using successor or predecessor *)
 
-Notation Zlt_succ_r := Z.lt_succ_r (compat "8.6").
-Notation Zle_succ_l := Z.le_succ_l (compat "8.6").
+Notation Zlt_succ_r := Z.lt_succ_r (compat "8.7").
+Notation Zle_succ_l := Z.le_succ_l (compat "8.7").
 
 Lemma Zgt_le_succ n m : m > n -> Z.succ n <= m.
 Proof.
@@ -336,8 +336,8 @@ Qed.
 
 (** Special cases of ordered integers *)
 
-Notation Zlt_0_1 := Z.lt_0_1 (compat "8.6").
-Notation Zle_0_1 := Z.le_0_1 (compat "8.6").
+Notation Zlt_0_1 := Z.lt_0_1 (compat "8.7").
+Notation Zle_0_1 := Z.le_0_1 (compat "8.7").
 
 Lemma Zle_neg_pos : forall p q:positive, Zneg p <= Zpos q.
 Proof.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index a9bc5bd09d..881ead1c4b 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -233,7 +233,7 @@ Qed.
 
 (** * Z.square: a direct definition of [z^2] *)
 
-Notation Psquare := Pos.square (compat "8.6").
-Notation Zsquare := Z.square (compat "8.6").
+Notation Psquare := Pos.square (compat "8.7").
+Notation Zsquare := Z.square (compat "8.7").
 Notation Psquare_correct := Pos.square_spec (only parsing).
 Notation Zsquare_correct := Z.square_spec (only parsing).
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 0c9aca2657..264109dc6f 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -37,17 +37,17 @@ Notation Ndiv_Zquot := N2Z.inj_quot (only parsing).
 Notation Nmod_Zrem := N2Z.inj_rem (only parsing).
 Notation Z_quot_rem_eq := Z.quot_rem' (only parsing).
 Notation Zrem_lt := Z.rem_bound_abs (only parsing).
-Notation Zquot_unique := Z.quot_unique (compat "8.6").
-Notation Zrem_unique := Z.rem_unique (compat "8.6").
-Notation Zrem_1_r := Z.rem_1_r (compat "8.6").
-Notation Zquot_1_r := Z.quot_1_r (compat "8.6").
-Notation Zrem_1_l := Z.rem_1_l (compat "8.6").
-Notation Zquot_1_l := Z.quot_1_l (compat "8.6").
-Notation Z_quot_same := Z.quot_same (compat "8.6").
+Notation Zquot_unique := Z.quot_unique (compat "8.7").
+Notation Zrem_unique := Z.rem_unique (compat "8.7").
+Notation Zrem_1_r := Z.rem_1_r (compat "8.7").
+Notation Zquot_1_r := Z.quot_1_r (compat "8.7").
+Notation Zrem_1_l := Z.rem_1_l (compat "8.7").
+Notation Zquot_1_l := Z.quot_1_l (compat "8.7").
+Notation Z_quot_same := Z.quot_same (compat "8.7").
 Notation Z_quot_mult := Z.quot_mul (only parsing).
-Notation Zquot_small := Z.quot_small (compat "8.6").
-Notation Zrem_small := Z.rem_small (compat "8.6").
-Notation Zquot2_quot := Zquot2_quot (compat "8.6").
+Notation Zquot_small := Z.quot_small (compat "8.7").
+Notation Zrem_small := Z.rem_small (compat "8.7").
+Notation Zquot2_quot := Zquot2_quot (compat "8.7").
 
 (** Particular values taken for [a÷0] and [(Z.rem a 0)].
     We avise to not rely on these arbitrary values. *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 1baaa8a45f..06d9ba3436 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -152,9 +152,9 @@ let add_vo_require opts d p export =
 
 let add_compat_require opts v =
   match v with
-  | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false)
   | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
-  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq88" 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)
 
 let set_batch_mode opts =
   Flags.quiet := true;
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 7dd5471f3f..cf69a84b8b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -60,10 +60,10 @@ let make_bullet s =
   | _ -> assert false
 
 let parse_compat_version = let open Flags in function
-  | "8.8" -> Current
+  | "8.9" -> Current
+  | "8.8" -> V8_8
   | "8.7" -> V8_7
-  | "8.6" -> V8_6
-  | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+  | ("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 ->