4 files changed, 29 insertions, 13 deletions
diff --git a/dev/base_include b/dev/base_include
index f2912e112..1da5e3ed1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -130,7 +130,6 @@ open Reserve
 open Syntax_def
 open Constrexpr
 open Constrexpr_ops
-open Topconstr
 open Notation_term
 open Notation_ops
 open Prettyp
@@ -231,7 +230,7 @@ let pf_e gl s =
 let _ = Flags.in_debugger := false
 let _ = Flags.in_toplevel := true
 let _ = Constrextern.set_extern_reference
-  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
+  (fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Id.Set.empty r));;
 
 let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc)
 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index cb1493d6a..168a34e6e 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -135,3 +135,9 @@
 ########################################################################
 : ${bignums_CI_BRANCH:=master}
 : ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
+
+########################################################################
+# Equations
+########################################################################
+: ${Equations_CI_BRANCH:=8.8+alpha}
+: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
new file mode 100755
index 000000000..f7470463d
--- /dev/null
+++ b/dev/ci/ci-equations.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Equations_CI_DIR=${CI_BUILD_DIR}/Equations
+
+git_checkout ${Equations_CI_BRANCH} ${Equations_CI_GITURL} ${Equations_CI_DIR}
+
+( cd ${Equations_CI_DIR} && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} && make -j ${NJOBS} test-suite && make -j ${NJOBS} examples && make install)
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index b4c8ae33c..0f496d3b9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -60,6 +60,7 @@ let pprecarg = function
 let ppwf_paths x = pp (Rtree.pp_tree pprecarg x)
 
 (* term printers *)
+let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma
 let rawdebug = ref false
 let ppevar evk = pp (str (Evd.string_of_existential evk))
 let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x))
@@ -69,9 +70,9 @@ let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.o
 let ppterm = ppconstr
 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 x))
-let pppattern = (fun x -> pp(pr_constr_pattern x))
-let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
+let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
+let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
+let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;
@@ -121,7 +122,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 term
+  pr_closure closure ++ (pr_lglob_constr_env Global.(env ())) term
 
 let ppclosure x = pp (pr_closure x)
 let ppclosedglobconstr x = pp (pr_closed_glob_constr x)
@@ -140,14 +141,14 @@ let safe_pr_global = function
 let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x
 
 let ppconst (sp,j) =
-    pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val)
+    pp (str"#" ++ KerName.print sp ++ str"=" ++ envpp pr_lconstr_env j.uj_val)
 
 let ppvar ((id,a)) =
-    pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a)
+    pp (str"#" ++ Id.print id ++ str":" ++ envpp pr_lconstr_env a)
 
 let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t)
 
-let ppj j = pp (genppj pr_ljudge j)
+let ppj j = pp (genppj (envpp pr_ljudge_env) j)
 
 let prsubst s = pp (Mod_subst.debug_pr_subst s)
 let prdelta s = pp (Mod_subst.debug_pr_delta s)
@@ -175,13 +176,13 @@ let ppclenv clenv = pp(pr_clenv clenv)
 let ppgoalgoal gl = pp(Goal.pr_goal gl)
 let ppgoal g = pp(Printer.pr_goal g)
 let ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Refiner.project g))
-let pphintdb db = pp(Hints.pr_hint_db db)
+let pphintdb db = pp(envpp Hints.pr_hint_db_env db)
 let ppproofview p =
   let gls,sigma = Proofview.proofview p in
   pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ pr_constr c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)
@@ -508,7 +509,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun _ -> in_current_context constr_display c)
+           (fun _ st -> in_current_context constr_display c; st)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
@@ -524,7 +525,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun _ -> in_current_context print_pure_constr c)
+           (fun _ st -> in_current_context print_pure_constr c; st)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)