6 files changed, 32 insertions, 50 deletions
diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml
index 40ae1a7b05..4f89bbd34e 100644
--- a/dev/checker_printers.ml
+++ b/dev/checker_printers.ml
@@ -59,15 +59,11 @@ let pP s = pp (hov 0 s)
 let ppuni u = pp(Universe.pr u)
 let ppuni_level u = pp (Level.pr u)
 
-let ppuniverse_set l = pp (LSet.pr l)
-let ppuniverse_instance l = pp (Instance.pr l)
-let ppauniverse_context l = pp (AUContext.pr Level.pr l)
 let ppuniverse_context l = pp (pr_universe_context Level.pr l)
 let ppconstraints c = pp (pr_constraints Level.pr c)
 let ppuniverse_context_future c =
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppuniverses u = pp (Univ.pr_universes u)
 
 let pploc x = let (l,r) = Loc.unloc x in
   print_string"(";print_int l;print_string",";print_int r;print_string")"
diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli
index 2f9500c5c3..8be9b87257 100644
--- a/dev/checker_printers.mli
+++ b/dev/checker_printers.mli
@@ -43,12 +43,8 @@ val ppididmap : Names.Id.t Names.Id.Map.t -> unit
 (* Universes *)
 val ppuni : Univ.Universe.t -> unit
 val ppuni_level : Univ.Level.t -> unit (* raw *)
-val ppuniverse_set : Univ.LSet.t -> unit
-val ppuniverse_instance : Univ.Instance.t -> unit
-val ppauniverse_context : Univ.AUContext.t -> unit
 val ppuniverse_context : Univ.UContext.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
-val ppuniverses : Univ.universes -> unit
 
 val pploc : Loc.t -> unit
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 098c950b32..4ddb582414 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2018-10-23-V1"
+# CACHEKEY: "bionic_coq-V2018-10-30-V1"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -53,8 +53,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM camlp5.$CAMLP5_VER
 
 # EDGE switch
-ENV COMPILER_EDGE="4.07.0" \
-    CAMLP5_VER_EDGE="7.06" \
+ENV COMPILER_EDGE="4.07.1" \
+    CAMLP5_VER_EDGE="7.06.10-g84ce6cc4" \
     COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \
     BASE_OPAM_EDGE="dune-release.1.1.0"
 
diff --git a/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh
new file mode 100644
index 0000000000..17eb5fffae
--- /dev/null
+++ b/dev/ci/user-overlays/08889-mattam-program-obl-subst.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8889" ] || [ "$CI_BRANCH" = "program-hook-obligation-subst" ]; then
+
+    Equations_CI_REF=program-hook-obligation-subst
+    Equations_CI_GITURL=https://github.com/mattam82/Coq-Equations
+
+fi
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index f45f6de529..cf95941de5 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -3,5 +3,5 @@
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
 (context (opam (switch 4.05.0+32bit)))
-(context (opam (switch 4.07.0)))
-(context (opam (switch 4.07.0+flambda)))
+(context (opam (switch 4.07.1)))
+(context (opam (switch 4.07.1+flambda)))
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index 85bb04efe0..d330f517be 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -14,40 +14,24 @@
 
 export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH
 
-GUESS_CHECKER=
-for arg in "$@"; do
-    if [ "${arg##*/}" = coqchk.byte ]; then
-        GUESS_CHECKER=1
-    fi
-done
-
-if [ -z "$GUESS_CHECKER" ]; then
-    exec $OCAMLDEBUG \
-	-I $CAMLP5LIB -I +threads \
-	-I $COQTOP \
-	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
-	-I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
-	-I $COQTOP/library -I $COQTOP/engine \
-	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
-        -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
-	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
-        -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
-        -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
-        -I $COQTOP/plugins/firstorder \
-        -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
-        -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
-        -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
-        -I $COQTOP/plugins/ring \
-	-I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
-        -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
-        -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
-        -I $COQTOP/ide \
-	"$@"
-else
-    exec $OCAMLDEBUG \
-        -I $CAMLP5LIB -I +threads \
-        -I $COQTOP \
-        -I $COQTOP/config -I $COQTOP/clib \
-        -I $COQTOP/lib -I $COQTOP/checker \
-        "$@"
-fi
+exec $OCAMLDEBUG \
+    -I $CAMLP5LIB -I +threads \
+    -I $COQTOP \
+    -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
+    -I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
+    -I $COQTOP/library -I $COQTOP/engine \
+    -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
+    -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
+    -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
+    -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
+    -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
+    -I $COQTOP/plugins/firstorder \
+    -I $COQTOP/plugins/funind     -I $COQTOP/plugins/groebner \
+    -I $COQTOP/plugins/interface  -I $COQTOP/plugins/micromega \
+    -I $COQTOP/plugins/omega      -I $COQTOP/plugins/quote \
+    -I $COQTOP/plugins/ring \
+    -I $COQTOP/plugins/rtauto     -I $COQTOP/plugins/setoid_ring \
+    -I $COQTOP/plugins/subtac     -I $COQTOP/plugins/syntax \
+    -I $COQTOP/plugins/xml        -I $COQTOP/plugins/ltac \
+    -I $COQTOP/ide \
+    "$@"