6 files changed, 44 insertions, 5 deletions
diff --git a/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh
new file mode 100644
index 0000000000..b05d02c5be
--- /dev/null
+++ b/dev/ci/user-overlays/07925-ppedrot-clean-transp-state.sh
@@ -0,0 +1,14 @@
+_OVERLAY_BRANCH=clean-transp-state
+
+if [ "$CI_PULL_REQUEST" = "7925" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then
+
+    unicoq_CI_REF="$_OVERLAY_BRANCH"
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+    equations_CI_REF="$_OVERLAY_BRANCH"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    mtac2_CI_REF="$_OVERLAY_BRANCH"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh
new file mode 100644
index 0000000000..08112d3054
--- /dev/null
+++ b/dev/ci/user-overlays/08902-ejgallego-ltac+use_atts_in_ast.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "8902" ] || [ "$CI_BRANCH" = "ltac+use_atts_in_ast" ]; then
+
+    aactactics_CI_REF=ltac+use_atts_in_ast
+    aactactics_CI_GITURL=https://github.com/ejgallego/aac-tactics
+
+    coqhammer_CI_REF=ltac+use_atts_in_ast
+    coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer
+
+    Equations_CI_REF=ltac+use_atts_in_ast
+    Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=ltac+use_atts_in_ast
+    mtac2_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh
new file mode 100644
index 0000000000..61ffa4a197
--- /dev/null
+++ b/dev/ci/user-overlays/09003-ejgallego-vernac+move_extend_ast.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "9003" ] || [ "$CI_BRANCH" = "vernac+move_extend_ast" ]; then
+
+    ltac2_CI_REF=vernac+move_extend_ast
+    ltac2_CI_GITURL=https://github.com/ejgallego/ltac2
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b1fdfafd3a..30a2967259 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -19,6 +19,10 @@ Names
   Constant.make3 has been removed, use Constant.make2
   Constant.repr3 has been removed, use Constant.repr2
 
+- `Names.transparent_state` has been moved to its own module `TransparentState`.
+  This module gathers utility functions that used to be defined in several
+  places.
+
 Coqlib:
 
 - Most functions from the `Coqlib` module have been deprecated in favor of
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f94e9acb72..4287702b3a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -514,18 +514,18 @@ let _ =
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in
-  let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in
+  let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
-  Vernacextend.vernac_extend ~command:"PrintConstr" [cmd]
+  vernac_extend ~command:"PrintConstr" [cmd]
 
 let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
   let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in
-  let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in
+  let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
-  Vernacextend.vernac_extend ~command:"PrintPureConstr" [cmd]
+  vernac_extend ~command:"PrintPureConstr" [cmd]
 
 (* Setting printer of unbound global reference *)
 open Names
diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 63d7d58053..eaa12ff702 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -101,7 +101,7 @@ val ppdelta : Mod_subst.delta_resolver -> unit
 
 val pp_idpred : Names.Id.Pred.t -> unit
 val pp_cpred : Names.Cpred.t -> unit
-val pp_transparent_state : Names.transparent_state -> unit
+val pp_transparent_state : TransparentState.t -> unit
 
 val pp_stack_t : Constr.t Reductionops.Stack.t -> unit
 val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit