From a4bde2c1504c3fa3efe74586798d5d6f372b40d9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 31 Aug 2018 19:51:50 -0400
Subject: Update dev/doc/release-process: compat+automate

As requested in
https://github.com/coq/coq/issues/8311#issuecomment-415976318
the release process describes the steps to take.

All automatable steps are taken by the new script
dev/tools/update-compat.py

I've tried to make the script relatively easy to update if functions get
renamed or moved, but since it's doing unstructured source manipulation,
it is sort-of fragile.

We could plausibly add a file to the test-suite to ensure that we catch
script-breakage early, but this would require dropping compatibility
support much earlier in the development cycle (the compatibility changes
would have to come right when the new version is branched, rather than
shortly before the beta release).
---
 .github/CODEOWNERS         |   3 +
 dev/doc/release-process.md |  30 +++-
 dev/tools/update-compat.py | 341 +++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 373 insertions(+), 1 deletion(-)
 create mode 100755 dev/tools/update-compat.py

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 267da478d7..29fe3ef20b 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -350,3 +350,6 @@
 
 /dev/tools/check-owners*.sh @SkySkimmer
 # Secondary maintainer @maximedenes
+
+/dev/tools/update-compat.py @JasonGross
+# Secondary maintainer @Zimmi48
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 1821a181f1..7765d4b05c 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -57,7 +57,35 @@
 ## Before the beta release date ##
 
 - [ ] Ensure the Credits chapter has been updated.
-- [ ] Ensure an empty `CompatXX.v` file has been created.
+- [ ] Ensure the compatibility infrastructure has been updated, which consists
+      of 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)
 - [ ] 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)
-- 
cgit v1.2.3


From 9e7402632f1aecf5d2dce936d95e296097024ea5 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 2 Oct 2018 14:40:52 -0400
Subject: Update compat notations to be compat 8.7

All changes done with

```
git grep --name-only 'compat "8.6"' | xargs sed -i s'/compat "8.6"/compat "8.7"/g'
```

As per https://github.com/coq/coq/pull/8374#issuecomment-426202818 and
https://github.com/coq/coq/issues/8383#issuecomment-426200497
---
 test-suite/bugs/closed/4798.v |  2 +-
 theories/Arith/Compare_dec.v  |  6 ++--
 theories/FSets/FMapFacts.v    |  2 +-
 theories/Init/Specif.v        | 26 +++++++-------
 theories/Logic/EqdepFacts.v   |  2 +-
 theories/NArith/BinNat.v      | 78 ++++++++++++++++++++---------------------
 theories/NArith/Ndec.v        |  4 +--
 theories/NArith/Ndiv_def.v    |  6 ++--
 theories/NArith/Nsqrt_def.v   |  8 ++---
 theories/PArith/BinPos.v      | 80 +++++++++++++++++++++----------------------
 theories/ZArith/BinInt.v      | 54 ++++++++++++++---------------
 theories/ZArith/ZArith_dec.v  |  2 +-
 theories/ZArith/Zabs.v        |  8 ++---
 theories/ZArith/Zcompare.v    | 14 ++++----
 theories/ZArith/Zdiv.v        |  6 ++--
 theories/ZArith/Zeven.v       |  4 +--
 theories/ZArith/Zmax.v        | 18 +++++-----
 theories/ZArith/Zmin.v        | 18 +++++-----
 theories/ZArith/Znumtheory.v  | 28 +++++++--------
 theories/ZArith/Zorder.v      | 28 +++++++--------
 theories/ZArith/Zpow_facts.v  |  4 +--
 theories/ZArith/Zquot.v       | 20 +++++------
 22 files changed, 209 insertions(+), 209 deletions(-)

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/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/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. *)
-- 
cgit v1.2.3


From 3208a68e2c1b5f29fe33b54a66a2c361d3bfc531 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Tue, 2 Oct 2018 14:45:00 -0400
Subject: Update the -compat flags

Mostly via `dev/tools/update-compat.py --cur-version=8.9`

We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).

We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).
---
 doc/stdlib/index-list.html.template              |   2 +-
 lib/flags.ml                                     |  10 +-
 lib/flags.mli                                    |   2 +-
 pretyping/pretyping.ml                           |   9 +-
 pretyping/unification.ml                         |   5 +-
 test-suite/bugs/closed/2378.v                    |  90 +--
 test-suite/bugs/closed/4306.v                    |   6 +-
 test-suite/output/PrintInfos.out                 |   4 +-
 test-suite/output/PrintInfos.v                   |   4 +-
 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v | 714 +++++++++++------------
 test-suite/success/Case11.v                      |   4 +-
 test-suite/success/Case17.v                      |  14 +-
 test-suite/success/CompatCurrentFlag.v           |   4 +-
 test-suite/success/CompatOldFlag.v               |   4 +-
 test-suite/success/CompatPreviousFlag.v          |   4 +-
 test-suite/success/FunindExtraction_compat86.v   | 506 ----------------
 test-suite/success/Injection.v                   |  12 +-
 test-suite/success/rewrite.v                     |   6 +-
 theories/Compat/Coq86.v                          |  15 -
 theories/Compat/Coq88.v                          |   2 +
 theories/Compat/Coq89.v                          |  11 +
 toplevel/coqargs.ml                              |   4 +-
 vernac/g_vernac.mlg                              |   6 +-
 23 files changed, 460 insertions(+), 978 deletions(-)
 delete mode 100644 test-suite/success/FunindExtraction_compat86.v
 delete mode 100644 theories/Compat/Coq86.v
 create mode 100644 theories/Compat/Coq89.v

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 162adf0626..d86c094b1f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -795,9 +795,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
@@ -896,10 +894,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/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/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/theories/Compat/Coq86.v b/theories/Compat/Coq86.v
deleted file mode 100644
index 666be207eb..0000000000
--- a/theories/Compat/Coq86.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(** Compatibility file for making Coq act similar to Coq v8.6 *)
-Require Export Coq.Compat.Coq87.
-
-Require Export Coq.extraction.Extraction.
-Require Export Coq.funind.FunInd.
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/Coq89.v b/theories/Compat/Coq89.v
new file mode 100644
index 0000000000..d25671887f
--- /dev/null
+++ b/theories/Compat/Coq89.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.9 *)
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 ->
-- 
cgit v1.2.3


From 425475e4605691642b09b625dd13e7e3506299b6 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 1 Sep 2018 20:05:07 -0400
Subject: Move the compat-update-process to right after branching

Also test that the compat updating script hasn't become outdated on the
CI.
---
 .github/CODEOWNERS                    |  1 +
 dev/doc/release-process.md            | 58 +++++++++++++++++------------------
 test-suite/Makefile                   | 23 +++++++++++++-
 test-suite/tools/update-compat/run.sh |  9 ++++++
 4 files changed, 61 insertions(+), 30 deletions(-)
 create mode 100755 test-suite/tools/update-compat/run.sh

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 29fe3ef20b..7ca407f36f 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -352,4 +352,5 @@
 # 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 7765d4b05c..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,35 +86,6 @@
 ## Before the beta release date ##
 
 - [ ] Ensure the Credits chapter has been updated.
-- [ ] Ensure the compatibility infrastructure has been updated, which consists
-      of 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)
 - [ ] 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/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/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 $?
-- 
cgit v1.2.3