7 files changed, 60 insertions, 25 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 7853866f62..4709247549 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -26,7 +26,8 @@ our CI. This means that:
 
 On the condition that:
 
-- At the time of the submission, your development works with Coq master branch.
+- At the time of the submission, your development works with Coq's
+  `master` branch.
 
 - Your development is publicly available in a git repository and we can easily
   send patches to you (e.g. through pull / merge requests).
@@ -60,6 +61,19 @@ performance benchmark. Currently this is done by providing an OPAM package
 in https://github.com/coq/opam-coq-archive and opening an issue at
 https://github.com/coq/coq-bench/issues.
 
+### Recommended branching policy.
+
+It is sometimes the case that you will need to maintain a branch of
+your development for particular Coq versions. This is in fact very
+likely if your development includes a Coq ML plugin.
+
+We thus recommend a branching convention that mirrors Coq's branching
+policy. Then, you would have a `master` branch that follows Coq's
+`master`, a `v8.8` branch that works with Coq's `v8.8` branch and so
+on.
+
+This convention will be supported by tools in the future to make some
+developer commands work more seamlessly.
 
 Information for developers
 --------------------------
diff --git a/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
new file mode 100644
index 0000000000..81ed91f52b
--- /dev/null
+++ b/dev/ci/user-overlays/08688-herbelin-master+generalizing-evar-map-printer-over-env.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8688" ] || [ "$CI_BRANCH" = "master+generalizing-evar-map-printer-over-env" ]; then
+
+    Elpi_CI_REF=master+generalized-evar-printers-pr8688
+    Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh
new file mode 100644
index 0000000000..8ad8cba243
--- /dev/null
+++ b/dev/ci/user-overlays/08844-split-tactics.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then
+    Equations_CI_REF=split-tactics
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    ltac2_CI_REF=split-tactics
+    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+    fiat_parsers_CI_REF=split-tactics
+    fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat
+fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 68afe7ee4a..7fb73e447d 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -33,3 +33,11 @@ fi
 ```
 
 (`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh))
+
+### Branching conventions
+
+We suggest you use the convention of identical branch names for the
+Coq branch and the CI project branch used in the overlay. For example,
+if your Coq PR is coming from the branch `more_efficient_tc`, and that
+breaks `ltac2`, we suggest you create a `ltac2` overlay with a branch
+named `more_efficient_tc`.
diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md
index 8f96ac223f..774552237a 100644
--- a/dev/doc/proof-engine.md
+++ b/dev/doc/proof-engine.md
@@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the
 `Refine.refine` primitive.
 
 ```ocaml
-val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
-(** In [refine typecheck t], [t] is a term with holes under some
+val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic
+(** In [refine ~typecheck t], [t] is a term with holes under some
     [evar_map] context. The term [t] is used as a partial solution
     for the current goal (refine is a goal-dependent tactic), the
     new holes created by [t] become the new subgoals. Exceptions
@@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic
     tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *)
 ```
 
-In a first approximation, we can think of `'a Sigma.run` as
-`evar_map -> 'a * evar_map`. What the function does is first evaluate the
-`Constr.t Sigma.run` argument in the current proof state, and then use the
-resulting term as a filler for the proof under focus. All evars that have been
-created by the invocation of this thunk are then turned into new goals added in
-the order of their creation.
+What the function does is first evaluate the `t` argument in the
+current proof state, and then use the resulting term as a filler for
+the proof under focus. All evars that have been created by the
+invocation of this thunk are then turned into new goals added in the
+order of their creation.
 
 To see how we can use it, let us have a look at an idealized example, the `cut`
 tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]`
@@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order.
 
 ```ocaml
 let cut c =
-  let open Sigma in
-  Proofview.Goal.nf_enter { enter = begin fun gl ->
+  Proofview.Goal.enter begin fun gl ->
     (** In this block, we focus on one goal at a time indicated by gl *)
     let env = Proofview.Goal.env gl in
     (** Get the context of the goal, essentially [Γ] *)
@@ -80,25 +78,22 @@ let cut c =
     let t = mkArrow c (Vars.lift 1 concl) in
     (** Build [X -> A]. Note the lifting of [A] due to being on the right hand
         side of the arrow. *)
-    Refine.refine { run = begin fun sigma ->
+    Refine.refine begin fun sigma ->
       (** All evars generated by this block will be added as goals *)
-      let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in
+      let sigma, f = Evarutil.new_evar env sigma t in
       (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the
           term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity
           substitution for [Γ] is extracted from the [env] argument, so that
           one must be careful to pass the correct context here in order for the
           resulting term to be well-typed. The [p] return value is a proof term
           used to enforce sigma monotonicity. *)
-      let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in
+      let sigma, x = Evarutil.new_evar env sigma c in
       (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return
           [x := Γ ⊢ ?e2{Γ} : X]. *)
       let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in
       (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *)
-      Sigma (r, sigma, p +> q)
-      (** Fills the current hole with [r]. The [p +> q] thingy ensures
-          monotonicity of sigma. *)
-    end }
-  end }
+    end
+  end
 ```
 
 The `Evarutil.new_evar` function is the preferred way to generate evars in
diff --git a/dev/tools/change-header b/dev/tools/change-header
index 61cc866602..687c02f4f1 100755
--- a/dev/tools/change-header
+++ b/dev/tools/change-header
@@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)'
 modified=0
 kept=0
 
-for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
+for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do
   headline=`head -n 1 $i`
   if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then
       # Has emacs header
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 44d44ccc4b..fd08f9ffe8 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -168,8 +168,8 @@ let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(Termops.pr_metaset metas)
-let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) evd)
-let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None evd)
+let ppevm evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes (Some 2) (Global.env ()) evd)
+let ppevmall evd = pp(Termops.pr_evar_map ~with_univs:!Detyping.print_universes None (Global.env ()) evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
@@ -180,14 +180,14 @@ let ppexistentialfilter filter = match Evd.Filter.repr filter with
 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 ppgoalsigma g = pp(Printer.pr_goal g ++ Termops.pr_evar_map None (Global.env ()) (Refiner.project g))
 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)
+  pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) (Global.env ()) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) (Global.env ()) evd ++ envpp pr_econstr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)