5 files changed, 44 insertions, 19 deletions
diff --git a/dev/ci/user-overlays/08515-command-atts.sh b/dev/ci/user-overlays/08515-command-atts.sh
new file mode 100755
index 0000000000..4605255d5e
--- /dev/null
+++ b/dev/ci/user-overlays/08515-command-atts.sh
@@ -0,0 +1,12 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8515" ] || [ "$CI_BRANCH" = "command-atts" ]; then
+    ltac2_CI_REF=command-atts
+    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+    Equations_CI_REF=command-atts
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    plugin_tutorial_CI_REF=command-atts
+    plugin_tutorial_CI_GITURL=https://github.com/SkySkimmer/plugin_tutorials
+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/doc/changes.md b/dev/doc/changes.md
index eb5b9ee1d3..b1fdfafd3a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -32,6 +32,12 @@ Macros:
 - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are
   deprecated. Use TYPED AS instead.
 
+- coqpp (.mlg) based VERNAC EXTEND accesses attributes through a `#[ x
+  = att ]` syntax, where `att : 'a Attributes.attribute` and `x` will
+  be bound with type `'a` in the expression, unlike the old system
+  where `atts : Vernacexpr.vernac_flags` was bound in the expression
+  and had to be manually parsed.
+
 ## Changes between Coq 8.8 and Coq 8.9
 
 ### ML API
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