11 files changed, 60 insertions, 57 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 10b4f9b044..98ea594366 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,12 +16,9 @@ We are currently running tests on the following platforms:
   `./configure`. It should allow complying with this discipline
   without pain.
 
-- AppVeyor is used to test the compilation of Coq and run the test-suite on
-  Windows.
-
 - Azure Pipelines is used to test the compilation of Coq and run the
-  test-suite on Windows and on macOS. It is expected to replace
-  appveyor eventually.
+  test-suite on Windows and on macOS. It is expected to be used to build
+  macOS and Windows packages eventually.
 
 You can anticipate the results of most of these tests prior to submitting your
 PR by running GitLab CI on your private branches. To do so follow these steps:
diff --git a/dev/ci/appveyor.bat b/dev/ci/appveyor.bat
deleted file mode 100644
index 341b875edc..0000000000
--- a/dev/ci/appveyor.bat
+++ /dev/null
@@ -1,42 +0,0 @@
-REM This script either runs the test suite with OPAM (if USEOPAM is true) or
-REM builds the Coq binary packages for windows (if USEOPAM is false).
-
-if %ARCH% == 32 (
-  SET ARCHLONG=i686
-  SET CYGROOT=C:\cygwin
-  SET SETUP=setup-x86.exe
-)
-
-if %ARCH% == 64 (
-  SET ARCHLONG=x86_64
-  SET CYGROOT=C:\cygwin64
-  SET SETUP=setup-x86_64.exe
-)
-
-SET CYGCACHE=%CYGROOT%\var\cache\setup
-SET APPVEYOR_BUILD_FOLDER_MFMT=%APPVEYOR_BUILD_FOLDER:\=/%
-SET APPVEYOR_BUILD_FOLDER_CFMT=%APPVEYOR_BUILD_FOLDER_MFMT:C:/=/cygdrive/c/%
-SET DESTCOQ=C:\coq%ARCH%_inst
-SET COQREGTESTING=Y
-
-if %USEOPAM% == false (
-  call %APPVEYOR_BUILD_FOLDER%\dev\build\windows\MakeCoq_MinGW.bat -threads=1 ^
-    -arch=%ARCH% -installer=Y -coqver=%APPVEYOR_BUILD_FOLDER_CFMT% ^
-    -destcyg=%CYGROOT% -destcoq=%DESTCOQ% -cygcache=%CYGCACHE% ^
-    -addon=bignums -make=N ^
-    -setup %CYGROOT%\%SETUP% || GOTO ErrorExit
-  copy "%CYGROOT%\build\coq-local\dev\nsis\*.exe" dev\nsis || GOTO ErrorExit
-  7z a coq-opensource-archive-windows-%ARCHLONG%.zip %CYGROOT%\build\tarballs\* || GOTO ErrorExit
-)
-
-if %USEOPAM% == true (
-  %CYGROOT%\%SETUP% -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% ^
-    -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time
-  %CYGROOT%/bin/bash -l %APPVEYOR_BUILD_FOLDER%/dev/ci/appveyor.sh || GOTO ErrorExit
-)
-
-GOTO :EOF
-
-:ErrorExit
-  ECHO ERROR %0 failed
-  EXIT /b 1
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 8dee465cf4..74e8d3bbaa 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -35,7 +35,7 @@
 : "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}"
 : "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}"
 
-: "${mtac2_CI_REF:=master-sync}"
+: "${mtac2_CI_REF:=master}"
 : "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}"
 : "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}"
 
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index baf470e021..4cd7faf757 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-12-14-V1"
+# CACHEKEY: "bionic_coq-V2019-01-28-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -38,7 +38,7 @@ ENV COMPILER="4.05.0"
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.3.0" \
-    CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8"
+    CI_OPAM="menhir.20181113 elpi.1.1.0 ocamlgraph.1.8.8"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2"
diff --git a/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
new file mode 100644
index 0000000000..6e89741e29
--- /dev/null
+++ b/dev/ci/user-overlays/06914-maximedenes-primitive-integers.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "6914" ] || [ "$CI_BRANCH" = "primitive-bool-list" ]; then
+
+    bignums_CI_REF=primitive-integers
+    bignums_CI_GITURL=https://github.com/vbgl/bignums
+
+    mtac2_CI_REF=primitive-integers
+    mtac2_CI_GITURL=https://github.com/vbgl/Mtac2
+
+fi
diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 29e87df6b8..8455d13377 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -10,7 +10,7 @@ In Coq source folder:
 opam switch 4.05.0+trunk+fp
 ./configure -local -debug
 make
-perf record -g bin/coqtop -compile file.v
+perf record -g bin/coqc file.v
 perf report -g fractal,callee --no-children
 
 To profile only part of a file, first load it using
@@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev
 
 ### For memory dump:
 
-CAMLRUNPARAM=T,mj bin/coqtop -compile file.v
+CAMLRUNPARAM=T,mj bin/coqc file.v
 
 In another terminal:
 
@@ -112,7 +112,7 @@ number of objects and third is the place where the objects where allocated.
 
 ### For complete memory graph:
 
-CAMLRUNPARAM=T,gr bin/coqtop -compile file.v
+CAMLRUNPARAM=T,gr bin/coqc file.v
 
 In another terminal:
 
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 8f9c3171da..1c4913d201 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -271,7 +271,7 @@ Coq ``V7'' archive & August 1999 & new cvs archive based on J.-C. Filliâtre's \
    & & \feature{kernel-centric} architecture \\
    & & more care for outside readers\\
    & & (indentation, ocaml warning protection)\\
-Coq V7.0beta& released 27 December 2000 & \feature{${\cal L}_{\mathit{tac}}$} \\
+Coq V7.0beta& released 27 December 2000 & \feature{${\mathcal{L}}_{\mathit{tac}}$} \\
 Coq V7.0beta2& released 2 February 2001\\
 
 Coq V7.0& released 25 April 2001 & \feature{extraction} (version 2) [6-2-2001] \\
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index 72e2930386..813ad71be9 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -143,7 +143,7 @@ fi
 # Sanity check: PR has an outdated version of CI
 
 BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha')
-CI_FILES=(".gitlab-ci.yml" "appveyor.yml")
+CI_FILES=(".gitlab-ci.yml" "azure-pipelines.yml")
 
 if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
 then
diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py
index bde00a2f0d..ff9b32fe78 100755
--- a/dev/tools/update-compat.py
+++ b/dev/tools/update-compat.py
@@ -74,6 +74,7 @@ COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml')
 G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg')
 DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template')
 BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v')
+BUG_9166_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_9166.v')
 TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh')
 TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i)
                          for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v'))
@@ -81,6 +82,9 @@ TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', '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))
+BUG_HEADER = r"""(* DO NOT MODIFY THIS FILE DIRECTLY *)
+(* It is autogenerated by %s. *)
+""" % os.path.relpath(os.path.realpath(__file__), ROOT_PATH)
 
 def get_header():
     with open(HEADER_PATH, 'r') as f: return f.read()
@@ -190,6 +194,15 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su
                 print_diff(contents, new_contents)
             raise Exception(exn_string % os.path.relpath(path, ROOT_PATH))
 
+def remove_if_exists(path, exn_string='%s exists when it should not!', assert_unchanged=False, **args):
+    if os.path.exists(path):
+        if not assert_unchanged:
+            print('Removing %s...' % os.path.relpath(path, ROOT_PATH))
+            os.remove(path)
+            maybe_git_rm(os.path.relpath(path, ROOT_PATH), **args)
+        else:
+            raise Exception(exn_string % os.path.relpath(path, ROOT_PATH))
+
 def update_file(new_contents, path, **args):
     update_if_changed(None, new_contents, path, **args)
 
@@ -343,7 +356,7 @@ def update_flags(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):
+def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TEST_SUITE_PATHS, test_suite_descriptions=TEST_SUITE_DESCRIPTIONS, test_suite_outdated_paths=tuple(), **args):
     assert(len(new_versions) == len(test_suite_paths))
     assert(len(new_versions) == len(test_suite_descriptions))
     for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)):
@@ -361,6 +374,8 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES
         lines.append('')
         new_contents = '\n'.join(lines)
         update_if_changed(contents, new_contents, path, suggest_add=suggest_add, **args)
+    for path in test_suite_outdated_paths:
+        remove_if_exists(path, assert_unchanged=assert_unchanged, **args)
 
 def update_doc_index(new_versions, **args):
     with open(DOC_INDEX_PATH, 'r') as f: contents = f.read()
@@ -391,12 +406,29 @@ def update_bug_4789(new_versions, **args):
     # 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.
+    new_contents = BUG_HEADER + 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_bug_9166(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_9166_PATH, 'r') as f: contents = f.read()
+    new_contents = BUG_HEADER + r"""Set Warnings "+deprecated".
+
+Notation bar := option (compat "%s").
+
+Definition foo (x: nat) : nat :=
+  match x with
+  | 0 => 0
+  | S bar => bar
+  end.
+""" % new_versions[0]
+    update_if_changed(contents, new_contents, BUG_9166_PATH, **args)
+
 def update_compat_notations_in(old_versions, new_versions, contents):
     for v in old_versions:
         if v not in new_versions:
@@ -469,6 +501,7 @@ if __name__ == '__main__':
     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_outdated_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)
@@ -476,5 +509,6 @@ if __name__ == '__main__':
     update_test_suite_run(**args)
     update_doc_index(new_versions, **args)
     update_bug_4789(new_versions, **args)
+    update_bug_9166(new_versions, **args)
     update_compat_notations(known_versions, new_versions, **args)
     display_git_grep(known_versions, new_versions)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 8f207d1e0a..2629cf8626 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -292,6 +292,8 @@ let constr_display csr =
       ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="")
         then (";"^i) else "")) lna "")^","
       ^(array_display bl)^")"
+  | Int i ->
+      "Int("^(Uint63.to_string i)^")"
 
   and array_display v =
     "[|"^
@@ -421,6 +423,8 @@ let print_pure_constr csr =
 	  print_cut();
         done
       in print_string"{"; print_fix (); print_string"}"
+  | Int i ->
+     print_string ("Int("^(Uint63.to_string i)^")")
 
   and box_display c = open_hovbox 1; term_display c; close_box()
 
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index ea126e2756..dc30793a6e 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -82,6 +82,7 @@ and ppwhd whd =
   | Vcofix _ -> print_string "cofix"
   | Vconstr_const i -> print_string "C(";print_int i;print_string")"
   | Vconstr_block b -> ppvblock b
+  | Vint64 i -> printf "int64(%LiL)" i
   | Vatom_stk(a,s) ->
       open_hbox();ppatom a;close_box();
       print_string"@";ppstack s