11 files changed, 52 insertions, 18 deletions
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 6cc91ace81..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
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-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 7942508698..85107780f1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-11-24-V91"
+# CACHEKEY: "bionic_coq-V2020-11-26-V92"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -43,7 +43,7 @@ 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="ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.11.4"
+    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"
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/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)