4 files changed, 16 insertions, 2 deletions
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/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