17 files changed, 250 insertions, 175 deletions

diff --git a/dev/bench/render_results b/dev/bench/render_results
index 72affd70b2..bd4308837b 100755
--- a/dev/bench/render_results
+++ b/dev/bench/render_results
@@ -76,25 +76,13 @@ let run_and_read cmd =
 ;;
 
 let ( %> ) f g x = g (f x)
-;;
 
 let run = run_and_read %> snd
-;;
 
 module Float = struct
   let nan = Pervasives.nan
 end
 
-module Tuple4 = struct
-
-  let first (x,_,_,_) = x
-  let second (_,y,_,_) = y
-  let third (_,_,z,_) = z
-  let fourth (_,_,_,z) = z
-
-end
-;;
-
 module List = struct
   include List
 
@@ -149,6 +137,151 @@ module String = struct
 end
 ;;
 
+module Table :
+sig
+  type header = string
+  type row = string list list
+  val print : header list -> row list -> string
+end =
+struct
+  type header = string
+
+  type row = string list list
+
+  let val_padding = 2
+  (* Padding between data in the same row *)
+  let row_padding = 1
+  (* Padding between rows *)
+
+  let homogeneous b = if b then () else failwith "Heterogeneous data"
+
+  let vert_split (ls : 'a list list) =
+    let split l = match l with
+    | [] -> failwith "vert_split"
+    | x :: l -> (x, l)
+    in
+    let ls = List.map split ls in
+    List.split ls
+
+  let rec last = function
+  | [] -> assert false
+  | [x] -> [], x
+  | x :: l ->
+    let (l, y) = last l in
+    (x :: l, y)
+
+  let justify n s =
+    let len = String.length s in
+    let () = assert (len <= n) in
+    let lft = (n - len) / 2 in
+    let rgt = n - lft - len in
+    String.make lft ' ' ^ s ^ String.make rgt ' '
+
+  let justify_row layout data =
+    let map n s =
+      let len = String.length s in
+      let () = assert (len <= n) in
+      (* Right align *)
+      let pad = n - len in
+      String.make pad ' ' ^ s
+    in
+    let data = List.map2 map layout data in
+    String.concat (String.make val_padding ' ') data
+
+  let angle hkind vkind = match hkind, vkind with
+  | `Lft, `Top -> "┌"
+  | `Rgt, `Top -> "┐"
+  | `Mid, `Top -> "┬"
+  | `Lft, `Mid -> "├"
+  | `Rgt, `Mid -> "┤"
+  | `Mid, `Mid -> "┼"
+  | `Lft, `Bot -> "└"
+  | `Rgt, `Bot -> "┘"
+  | `Mid, `Bot -> "┴"
+
+  let print_separator vkind col_size =
+    let rec dashes n = if n = 0 then "" else "─" ^ dashes (n - 1) in
+    let len = List.length col_size in
+    let pad = dashes row_padding in
+    let () = assert (0 < len) in
+    let map n = dashes n in
+    angle `Lft vkind ^ pad ^
+    String.concat (pad ^ angle `Mid vkind ^ pad) (List.map map col_size) ^
+    pad ^ angle `Rgt vkind
+
+  let print_blank col_size =
+    let len = List.length col_size in
+    let () = assert (0 < len) in
+    let pad = String.make row_padding ' ' in
+    let map n = String.make n ' ' in
+    "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) (List.map map col_size) ^ pad ^ "│"
+
+  let print_row row =
+    let len = List.length row in
+    let () = assert (0 < len) in
+    let pad = String.make row_padding ' ' in
+    "│" ^ pad ^ String.concat (pad ^ "│" ^ pad) row ^ pad ^ "│"
+
+  (* Invariant : all rows must have the same shape *)
+
+  let print (headers : header list) (rows : row list) =
+    (* Sanitize input *)
+    let ncolums = List.length headers in
+    let shape = ref None in
+    let check row =
+      let () = homogeneous (List.length row = ncolums) in
+      let rshape : int list = List.map (fun data -> List.length data) row in
+      match !shape with
+      | None -> shape := Some rshape
+      | Some s -> homogeneous (rshape = s)
+    in
+    let () = List.iter check rows in
+    (* Compute layout *)
+    let rec layout n (rows : row list) =
+      if n = 0 then []
+      else
+        let (col, rows) = vert_split rows in
+        let ans = layout (n - 1) rows in
+        let data = ref None in
+        let iter args =
+          let size = List.map String.length args in
+          match !data with
+          | None -> data := Some size
+          | Some s ->
+            data := Some (List.map2 (fun len1 len2 -> max len1 len2) s size)
+        in
+        let () = List.iter iter col in
+        let data = match !data with None -> [] | Some s -> s in
+        data :: ans
+    in
+    let layout = layout ncolums rows in
+    let map hd shape =
+      let data_size = match shape with
+      | [] -> 0
+      | n :: shape -> List.fold_left (fun accu n -> accu + n + val_padding) n shape
+      in
+      max (String.length hd) data_size
+    in
+    let col_size = List.map2 map headers layout in
+    (* Justify the data *)
+    let headers = List.map2 justify col_size headers in
+    let rows = List.map (fun row -> List.map2 justify col_size (List.map2 justify_row layout row)) rows in
+    (* Print the table *)
+    let rows, last = last rows in
+    let sep = print_separator `Mid col_size in
+    let rows = List.concat @@ List.map (fun r -> [print_row r; sep]) rows in
+    let lines =
+      print_separator `Top col_size ::
+      print_row headers ::
+      print_blank col_size ::
+      rows @
+      print_row last ::
+      print_separator `Bot col_size ::
+      []
+    in
+    String.concat "\n" lines
+end
+
 (******************************************************************************)
 (* END Copied from batteries, to remove *)
 (******************************************************************************)
@@ -203,10 +336,6 @@ let proportional_difference_of_integers new_value old_value =
   else float_of_int (new_value - old_value) /. float_of_int old_value *. 100.0
 in
 
-let count_number_of_digits_before_decimal_point =
-  log10 %> floor %> int_of_float %> succ %> max 1
-in
-
 (* parse the *.time and *.perf files *)
 coq_opam_packages
 |> List.map
@@ -259,138 +388,39 @@ coq_opam_packages
 
 (* Below we take the measurements and format them to stdout. *)
 
+|> List.map begin fun (package_name, new_t, old_t, perc) ->
+
+  let precision = 2 in
+  let prf f = Printf.sprintf "%.*f" precision f in
+  let pri n = Printf.sprintf "%d" n in
+
+  [
+    [ package_name ];
+    [ prf new_t.user_time; prf old_t.user_time; prf perc.user_time ];
+    [ pri new_t.num_cycles; pri old_t.num_cycles; prf perc.num_cycles ];
+    [ pri new_t.num_instr; pri old_t.num_instr; prf perc.num_instr ];
+    [ pri new_t.num_mem; pri old_t.num_mem; prf perc.num_mem ];
+    [ pri new_t.num_faults; pri old_t.num_faults; prf perc.num_faults ];
+  ]
+
+  end
+
 |> fun measurements ->
 
-     let precision = 2 in
-
-     (* the labels that we will print *)
-     let package_name__label = "package_name" in
-     let new__label = "NEW" in
-     let old__label = "OLD" in
-     let proportional_difference__label = "PDIFF" in
-
-     (* the lengths of labels that we will print *)
-     let new__label__length = String.length new__label in
-     let proportional_difference__label__length = String.length proportional_difference__label in
-
-     (* widths of individual columns of the table *)
-     let package_name__width =
-       max (measurements |> List.map (Tuple4.first %> String.length) |> List.max)
-         (String.length package_name__label) in
-
-     let llf proj =
-       let lls = count_number_of_digits_before_decimal_point (List.max proj) + 1 + precision in
-       max lls new__label__length in
-
-     let lli proj =
-       let lls = count_number_of_digits_before_decimal_point (float_of_int (List.(max proj))) + 1 + precision in
-       max lls new__label__length in
-
-     let new_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.second measurements in
-     let old_timing_width = reduce_pkg_timings llf lli @@ List.map Tuple4.third measurements in
-
-     let llp proj =
-       let lls =
-         count_number_of_digits_before_decimal_point List.(max List.(map abs_float proj)) + 2 + precision in
-       max lls proportional_difference__label__length in
-
-     let perc_timing_width = reduce_pkg_timings llp llp @@ List.map Tuple4.fourth measurements in
-
-     (* print the table *)
-     let rec make_dashes = function
-       | 0 -> ""
-       | count -> "─" ^ make_dashes (pred count)
-     in
-
-     let vertical_separator left_glyph middle_glyph right_glyph =
-       sprintf "%s─%s─%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s─%s─%s─%s───%s\n"
-       left_glyph
-       (make_dashes package_name__width)
-       middle_glyph
-       (make_dashes new_timing_width.user_time)
-       (make_dashes old_timing_width.user_time)
-       (make_dashes perc_timing_width.user_time)
-       middle_glyph
-       (make_dashes new_timing_width.num_cycles)
-       (make_dashes old_timing_width.num_cycles)
-       (make_dashes perc_timing_width.num_cycles)
-       middle_glyph
-       (make_dashes new_timing_width.num_instr)
-       (make_dashes old_timing_width.num_instr)
-       (make_dashes perc_timing_width.num_instr)
-       middle_glyph
-       (make_dashes new_timing_width.num_mem)
-       (make_dashes old_timing_width.num_mem)
-       (make_dashes perc_timing_width.num_mem)
-       middle_glyph
-       (make_dashes new_timing_width.num_faults)
-       (make_dashes old_timing_width.num_faults)
-       (make_dashes perc_timing_width.num_faults)
-       right_glyph
-     in
-
-     let center_string string width =
-       let string_length = String.length string in
-       let width = max width string_length in
-       let left_hfill = (width - string_length) / 2 in
-       let right_hfill = width - left_hfill - string_length in
-       String.make left_hfill ' ' ^ string ^ String.make right_hfill ' '
-     in
-     printf "\n";
-     print_string (vertical_separator "┌" "┬" "┐");
-     "│" ^ String.make (1 + package_name__width + 1) ' ' ^ "│"
-     ^ center_string "user time [s]" (1 +  new_timing_width.user_time + 1 + old_timing_width.user_time + 1 + perc_timing_width.user_time + 3) ^ "│"
-     ^ center_string "CPU cycles" (1 + new_timing_width.num_cycles    + 1 + old_timing_width.num_cycles    + 1 + perc_timing_width.num_cycles + 3) ^ "│"
-     ^ center_string "CPU instructions" (1 + new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ^ "│"
-     ^ center_string "max resident mem [KB]" (1 + new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ^ "│"
-     ^ center_string "mem faults" (1 + new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3)
-     ^ "│\n" |> print_string;
-     printf "│%*s │ %*s│ %*s│ %*s│ %*s│ %*s│\n"
-       (1 + package_name__width) ""
-       (new_timing_width.user_time    + 1 + old_timing_width.user_time    + 1 + perc_timing_width.user_time + 3) ""
-       (new_timing_width.num_cycles       + 1 + old_timing_width.num_cycles       + 1 + perc_timing_width.num_cycles + 3) ""
-       (new_timing_width.num_instr + 1 + old_timing_width.num_instr + 1 + perc_timing_width.num_instr + 3) ""
-       (new_timing_width.num_mem + 1 + old_timing_width.num_mem + 1 + perc_timing_width.num_mem + 3) ""
-       (new_timing_width.num_faults + 1 + old_timing_width.num_faults + 1 + perc_timing_width.num_faults + 3) "";
-     printf "│ %*s │ %*s %*s %*s   │ %*s %*s %*s   │ %*s %*s %*s   │ %*s %*s %*s   │ %*s %*s %*s   │\n"
-       package_name__width package_name__label
-       new_timing_width.user_time new__label
-       old_timing_width.user_time old__label
-       perc_timing_width.user_time proportional_difference__label
-       new_timing_width.num_cycles new__label
-       old_timing_width.num_cycles old__label
-       perc_timing_width.num_cycles proportional_difference__label
-       new_timing_width.num_instr new__label
-       old_timing_width.num_instr old__label
-       perc_timing_width.num_instr proportional_difference__label
-       new_timing_width.num_mem new__label
-       old_timing_width.num_mem old__label
-       perc_timing_width.num_mem proportional_difference__label
-       new_timing_width.num_faults new__label
-       old_timing_width.num_faults old__label
-       perc_timing_width.num_faults proportional_difference__label;
-     measurements |> List.iter
-         (fun (package_name, new_t, old_t, perc) ->
-           print_string (vertical_separator "├" "┼" "┤");
-           printf "│ %*s │ %*.*f %*.*f %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │ %*d %*d %+*.*f %% │\n"
-             package_name__width package_name
-             new_timing_width.user_time precision new_t.user_time
-             old_timing_width.user_time precision old_t.user_time
-             perc_timing_width.user_time precision perc.user_time
-             new_timing_width.num_cycles new_t.num_cycles
-             old_timing_width.num_cycles old_t.num_cycles
-             perc_timing_width.num_cycles precision perc.num_cycles
-             new_timing_width.num_instr new_t.num_instr
-             old_timing_width.num_instr old_t.num_instr
-             perc_timing_width.num_instr precision perc.num_instr
-             new_timing_width.num_mem new_t.num_mem
-             old_timing_width.num_mem old_t.num_mem
-             perc_timing_width.num_mem precision perc.num_mem
-             new_timing_width.num_faults new_t.num_faults
-             old_timing_width.num_faults old_t.num_faults
-             perc_timing_width.num_faults precision perc.num_faults);
-
-print_string (vertical_separator "└" "┴" "┘");
+    let headers = [
+      "";
+      "user time [s]";
+      "CPU cycles";
+      "CPU instructions";
+      "max resident mem [KB]";
+      "mem faults";
+    ] in
+
+    let descr = ["NEW"; "OLD"; "PDIFF"] in
+    let top = [ [ "package_name" ]; descr; descr; descr; descr; descr ] in
+
+    printf "%s%!" (Table.print headers (top :: measurements))
+;
 
 (* ejgallego: disable this as it is very verbose and brings up little info in the log. *)
 if false then begin
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 6f6b3cd6d2..ebbf10f548 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1200,7 +1200,7 @@ function make_elpi {
   make_dune
   make_re
 
-  if build_prep https://github.com/LPCIC/elpi/archive v1.11.4 tar.gz 1 elpi; then
+  if build_prep https://github.com/LPCIC/elpi/archive v1.12.0 tar.gz 1 elpi; then
 
     log2 dune build -p elpi
     log2 dune install elpi
@@ -1749,7 +1749,7 @@ function make_addon_compcert {
   installer_addon_dependency_end
   if build_prep_overlay compcert; then
     installer_addon_section compcert "CompCert" "ATTENTION: THIS IS NOT OPEN SOURCE! CompCert verified C compiler and Clightgen (required for using VST for your own code)" "off"
-    logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin
+    logn configure ./configure -ignore-coq-version -clightgen -prefix "$PREFIXCOQ" -coqdevdir "$PREFIXCOQ/lib/coq/user-contrib/compcert" x86_32-cygwin -use-external-MenhirLib -use-external-Flocq
     log1 make $MAKE_OPT
     log2 make install
     logn install-license-1 install -D -T  "LICENSE" "$PREFIXCOQ/lib/coq/user-contrib/compcert/LICENSE"
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 75d9efaadc..18fdd83218 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -306,7 +306,7 @@
 # menhirlib
 ########################################################################
 # Note: menhirlib is now in subfolder coq-menhirlib of menhir
-: "${menhirlib_CI_REF:=master}"
+: "${menhirlib_CI_REF:=20201122}"
 : "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}"
 : "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}"
 
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index b85261d7fc..1a4ebc0e90 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -19,20 +19,20 @@ then
 elif [ -d "$PWD/_build/install/default/" ];
 then
     # Dune build
-    export OCAMLPATH="$PWD/_build/install/default/lib/:$OCAMLPATH"
+    export OCAMLPATH="$PWD/_build/install/default/lib/:$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/_build/install/default/bin"
     export COQLIB="$PWD/_build/install/default/lib/coq"
     CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
     export CI_BRANCH
 else
     # We assume we are in `-profile devel` build, thus `-local` is set
-    export OCAMLPATH="$PWD:$OCAMLPATH"
+    export OCAMLPATH="$PWD:$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/bin"
     CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
     export CI_BRANCH
 fi
 
-export PATH="$COQBIN:$PATH"
+export PATH="$COQBIN:$PWD/_install_ci/bin:$PATH"
 
 # Coq's tools need an ending slash :S, we should fix them.
 export COQBIN="$COQBIN/"
@@ -42,6 +42,9 @@ ls -l "$COQBIN"
 # Where we download and build external developments
 CI_BUILD_DIR="$PWD/_build_ci"
 
+# Where we install external binaries and ocaml libraries
+CI_INSTALL_DIR="$PWD/_install_ci"
+
 ls -l "$CI_BUILD_DIR" || true
 
 declare -A overlays
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index 6b09726606..3c8d65f5c1 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -7,6 +7,6 @@ git_download compcert
 
 export COQCOPTS='-native-compiler no -w -undeclared-scope -w -omega-is-deprecated'
 ( cd "${CI_BUILD_DIR}/compcert" && \
-      ./configure -ignore-coq-version x86_32-linux && \
+      ./configure -ignore-coq-version x86_32-linux -use-external-MenhirLib -use-external-Flocq && \
       make && \
       make check-proof COQCHK='"$(COQBIN)coqchk" -silent -o $(COQINCLUDES)')
diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh
index ffe92dcecf..777d36a6d7 100755
--- a/dev/ci/ci-coquelicot.sh
+++ b/dev/ci/ci-coquelicot.sh
@@ -3,8 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-install_ssreflect
-
 git_download coquelicot
 
-( cd "${CI_BUILD_DIR}/coquelicot" && autoreconf -i -s && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/coquelicot" && ( if [ ! -x ./configure ]; then autoreconf -i -s && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index a3a704091b..cb6c3e6452 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download flocq
 
-( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
+( cd "${CI_BUILD_DIR}/flocq" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-fourcolor.sh b/dev/ci/ci-fourcolor.sh
new file mode 100755
index 0000000000..72a1567398
--- /dev/null
+++ b/dev/ci/ci-fourcolor.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download fourcolor
+
+( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
diff --git a/dev/ci/ci-interval.sh b/dev/ci/ci-interval.sh
new file mode 100755
index 0000000000..fe7b3f9fbe
--- /dev/null
+++ b/dev/ci/ci-interval.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download interval
+
+export COQEXTRAFLAGS='-native-compiler no'
+( cd "${CI_BUILD_DIR}/interval" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-mathcomp.sh b/dev/ci/ci-mathcomp.sh
index b1aa56ec4e..f170b35327 100755
--- a/dev/ci/ci-mathcomp.sh
+++ b/dev/ci/ci-mathcomp.sh
@@ -7,11 +7,3 @@ ci_dir="$(dirname "$0")"
 git_download mathcomp
 
 ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make test-suite && make install )
-
-git_download fourcolor
-
-( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
-
-git_download oddorder
-
-( cd "${CI_BUILD_DIR}/oddorder" && make )
diff --git a/dev/ci/ci-menhir.sh b/dev/ci/ci-menhir.sh
new file mode 100755
index 0000000000..5ad78383d8
--- /dev/null
+++ b/dev/ci/ci-menhir.sh
@@ -0,0 +1,8 @@
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download menhirlib
+
+( cd "${CI_BUILD_DIR}/menhirlib" && dune build @install -p menhirLib,menhirSdk,menhir && dune install -p menhirLib,menhirSdk,menhir menhir menhirSdk menhirLib --prefix=${CI_INSTALL_DIR} )
+
+( cd "${CI_BUILD_DIR}/menhirlib" && make -C coq-menhirlib && make -C coq-menhirlib install )
diff --git a/dev/ci/ci-oddorder.sh b/dev/ci/ci-oddorder.sh
new file mode 100755
index 0000000000..b2da32ad61
--- /dev/null
+++ b/dev/ci/ci-oddorder.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download oddorder
+
+( cd "${CI_BUILD_DIR}/oddorder" && make && make install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index c17ec502e7..85107780f1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-10-12-V89"
+# CACHEKEY: "bionic_coq-V2020-11-26-V92"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -42,8 +42,8 @@ ENV COMPILER="4.05.0"
 
 # Common OPAM packages
 ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \
-    CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.11.4"
+    CI_OPAM="ocamlgraph.1.8.8" \
+    BASE_ONLY_OPAM="elpi.1.12.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
@@ -62,7 +62,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.11.1" \
-    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.15.0"
+    BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
 # `ci-template-flambda` with everything.
diff --git a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh
new file mode 100644
index 0000000000..0bf806085e
--- /dev/null
+++ b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then
+
+    overlay equations https://github.com/SkySkimmer/Coq-Equations intern-univs
+
+    overlay paramcoq https://github.com/SkySkimmer/paramcoq intern-univs
+
+    overlay elpi https://github.com/SkySkimmer/coq-elpi intern-univs
+fi
diff --git a/dev/ci/user-overlays/13481-elpi-1.12.sh b/dev/ci/user-overlays/13481-elpi-1.12.sh
new file mode 100644
index 0000000000..a6be2e3a1a
--- /dev/null
+++ b/dev/ci/user-overlays/13481-elpi-1.12.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "13481" ] || [ "$CI_BRANCH" = "elpi-1.12" ]; then
+
+    elpi_CI_REF=coq-master+elpi.1.12
+    elpi_hb_CI_REF=coq-master+coq-elpi-1.7.0+elpi-1.12
+
+fi
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index 2e8a7455de..7701264ad1 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -9,10 +9,10 @@
 
 CODE=0
 
-if [[ $(git log -n 1 --pretty='format:%s') == "Bot merge"* ]]; then
-    # The FIRST parent of bot merges is from the PR, the second is
+if [[ $(git log -n 1 --pretty='format:%s') == "[CI merge]"* ]]; then
+    # The second parent of bot merges is from the PR, the first is
     # current master
-    head=$(git rev-parse HEAD~)
+    head=$(git rev-parse HEAD^2)
 else
     head=$(git rev-parse HEAD)
 fi
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a9438c4aca..4faa12af79 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -27,6 +27,11 @@ let _ = Detyping.print_evar_arguments := true
 let _ = Detyping.print_universes := true
 let _ = Goptions.set_bool_option_value ["Printing";"Matching"] false
 
+let with_env_evm f x =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  f env sigma x
+
 (* std_ppcmds *)
 let pp   x = Pp.pp_with !Topfmt.std_ft x
 
@@ -75,7 +80,7 @@ let ppeconstr x = pp (pr_econstr x)
 let ppconstr_expr x = let sigma,env = get_current_context () in pp (Ppconstr.pr_constr_expr env sigma x)
 let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
-let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
+let ppglob_constr = (fun x -> pp(with_env_evm pr_lglob_constr_env x))
 let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
@@ -130,7 +135,7 @@ let rec pr_closure {idents=idents;typed=typed;untyped=untyped} =
 and pr_closed_glob_constr_idmap x =
   pridmap (fun _ -> pr_closed_glob_constr) x
 and pr_closed_glob_constr {closure=closure;term=term} =
-  pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term
+  pr_closure closure ++ with_env_evm pr_lglob_constr_env term
 
 let ppclosure x = pp (pr_closure x)
 let ppclosedglobconstr x = pp (pr_closed_glob_constr x)
@@ -212,7 +217,7 @@ let pproof p = pp(Proof.pr_proof p)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let prlev = UnivNames.pr_with_global_universes
+let prlev = UnivNames.pr_with_global_universes Id.Map.empty
 let ppuniverse_set l = pp (LSet.pr prlev l)
 let ppuniverse_instance l = pp (Instance.pr prlev l)
 let ppuniverse_context l = pp (pr_universe_context prlev l)