diff --git a/doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst b/doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst
new file mode 100644
index 000000000000..e96bc2524591
--- /dev/null
+++ b/doc/changelog/06-Ltac2-language/21558-ltac2-transparent-state-Added.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Low-level operations to manipulate transparent states:
+  1. Set-like operations (union, intersection, difference).
+  2. Operations to add/remove/test membership of constants, variables, and primitive projections.
+  (`#21558 <https://github.com/rocq-prover/rocq/pull/21558>`_,
+  by Mathis Bouverot-Dupuis).
diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml
index d968a1a70bd8..b9e727b2311c 100644
--- a/plugins/ltac2/tac2stdlib.ml
+++ b/plugins/ltac2/tac2stdlib.ml
@@ -710,16 +710,94 @@ let () =
 
 (** Tactics for [Ltac2/TransparentState.v]. *)
 
+let () =
+  define "empty_transparent_state" (ret transparent_state) TransparentState.empty
+
+let () =
+  define "full_transparent_state" (ret transparent_state) TransparentState.full
+
 let () =
   define "current_transparent_state"
     (unit @-> tac transparent_state)
     Tac2tactics.current_transparent_state
 
 let () =
-  define "full_transparent_state" (ret transparent_state) TransparentState.full
+  define "union_transparent_state"
+    (transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
+    { tr_var = Id.Pred.union ts1.tr_var ts2.tr_var ;
+      tr_cst = Cpred.union ts1.tr_cst ts2.tr_cst ;
+      tr_prj = PRpred.union ts1.tr_prj ts2.tr_prj }
 
 let () =
-  define "empty_transparent_state" (ret transparent_state) TransparentState.empty
+  define "inter_transparent_state"
+    (transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
+    { tr_var = Id.Pred.inter ts1.tr_var ts2.tr_var ;
+      tr_cst = Cpred.inter ts1.tr_cst ts2.tr_cst ;
+      tr_prj = PRpred.inter ts1.tr_prj ts2.tr_prj }
+
+let () =
+  define "diff_transparent_state"
+    (transparent_state @-> transparent_state @-> ret transparent_state) @@ fun ts1 ts2 ->
+    { tr_var = Id.Pred.diff ts1.tr_var ts2.tr_var ;
+      tr_cst = Cpred.diff ts1.tr_cst ts2.tr_cst ;
+      tr_prj = PRpred.diff ts1.tr_prj ts2.tr_prj }
+
+let () =
+  define "add_constant_transparent_state"
+    (constant @-> transparent_state @-> ret transparent_state) @@ fun c ts ->
+    { tr_var = ts.tr_var ;
+      tr_cst = Cpred.add c ts.tr_cst ;
+      tr_prj = ts.tr_prj }
+
+let () =
+  define "add_proj_transparent_state"
+    (projection @-> transparent_state @-> ret transparent_state) @@ fun p ts ->
+    { tr_var = ts.tr_var ;
+      tr_cst = ts.tr_cst ;
+      tr_prj = PRpred.add (Projection.repr p) ts.tr_prj }
+
+let () =
+  define "add_var_transparent_state"
+    (ident @-> transparent_state @-> ret transparent_state) @@ fun v ts ->
+    { tr_var = Id.Pred.add v ts.tr_var ;
+      tr_cst = ts.tr_cst ;
+      tr_prj = ts.tr_prj }
+
+let () =
+  define "remove_constant_transparent_state"
+    (constant @-> transparent_state @-> ret transparent_state) @@ fun c ts ->
+    { tr_var = ts.tr_var ;
+      tr_cst = Cpred.remove c ts.tr_cst ;
+      tr_prj = ts.tr_prj }
+
+let () =
+  define "remove_proj_transparent_state"
+    (projection @-> transparent_state @-> ret transparent_state) @@ fun p ts ->
+    { tr_var = ts.tr_var ;
+      tr_cst = ts.tr_cst ;
+      tr_prj = PRpred.remove (Projection.repr p) ts.tr_prj }
+
+let () =
+  define "remove_var_transparent_state"
+    (ident @-> transparent_state @-> ret transparent_state) @@ fun v ts ->
+    { tr_var = Id.Pred.remove v ts.tr_var ;
+      tr_cst = ts.tr_cst ;
+      tr_prj = ts.tr_prj }
+
+let () =
+  define "mem_constant_transparent_state"
+    (constant @-> transparent_state @-> ret bool) @@ fun c ts ->
+    Cpred.mem c ts.tr_cst
+
+let () =
+  define "mem_proj_transparent_state"
+    (projection @-> transparent_state @-> ret bool) @@ fun p ts ->
+    PRpred.mem (Projection.repr p) ts.tr_prj
+
+let () =
+  define "mem_var_transparent_state"
+    (ident @-> transparent_state @-> ret bool) @@ fun v ts ->
+    Id.Pred.mem v ts.tr_var
 
 (** Tactics around Evarconv unification (in [Ltac2/Unification.v]). *)
 
diff --git a/theories/Ltac2/TransparentState.v b/theories/Ltac2/TransparentState.v
index 20cfdba2e8bd..dec7da365743 100644
--- a/theories/Ltac2/TransparentState.v
+++ b/theories/Ltac2/TransparentState.v
@@ -10,7 +10,8 @@
 
 Require Import Ltac2.Init.
 
-(** Abstract type representing a transparency state. *)
+(** Abstract type representing a transparency state. A transparency state
+    is a set of variables, constants, and primitive projections.  *)
 Ltac2 Type t.
 
 (** [empty] is the empty transparency state (all constants are opaque). *)
@@ -25,3 +26,63 @@ Ltac2 @ external full : t :=
     by, e.g., the [Strategy] command, or the [with_strategy] Ltac tactic. *)
 Ltac2 @ external current : unit -> t :=
   "rocq-runtime.plugins.ltac2" "current_transparent_state".
+
+(** [union t1 t2] builds a transparency state containing all the variables,
+    constants, and primitive projections which are either in [t1] or in [t2]. *)
+Ltac2 @ external union : t -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "union_transparent_state".
+
+(** [inter t1 t2] builds a transparency state containing all the variables,
+    constants, and primitive projections which are both in [t1] and in [t2]. *)
+Ltac2 @ external inter : t -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "inter_transparent_state".
+
+(** [diff t1 t2] builds a transparency state containing all the variables,
+    constants, and primitive projections which are in [t1] but not in [t2]. *)
+Ltac2 @ external diff : t -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "diff_transparent_state".
+
+(** [add_constant c t] adds the constant [c] to the transparency state [t].
+    Does nothing if the constant is already present. *)
+Ltac2 @ external add_constant : constant -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "add_constant_transparent_state".
+
+(** [add_proj p t] adds the primitive projection [p] to the transparency
+    state [t]. Does nothing if the projection is already present. *)
+Ltac2 @ external add_proj : projection -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "add_proj_transparent_state".
+
+(** [add_var p t] adds the local variable [v] to the transparency state [t].
+    Does nothing if the variable is already present. *)
+Ltac2 @ external add_var : ident -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "add_var_transparent_state".
+
+(** [remove_constant c t] removes the constant [c] from the transparency
+    state [t]. Does nothing if the constant is not present. *)
+Ltac2 @ external remove_constant : constant -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "remove_constant_transparent_state".
+
+(** [remove_proj p t] removes the primitive projection [p] from the
+    transparency state [t]. Does nothing if the projection is not present. *)
+Ltac2 @ external remove_proj : projection -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "remove_proj_transparent_state".
+
+(** [remove_var p t] removes the local variable [v] from the transparency
+    state [t]. Does nothing if the variable is not present. *)
+Ltac2 @ external remove_var : ident -> t -> t :=
+  "rocq-runtime.plugins.ltac2" "remove_var_transparent_state".
+
+(** [mem_constant c t] checks whether the constant [c] is present in the
+    transparency state [t]. *)
+Ltac2 @ external mem_constant : constant -> t -> bool :=
+  "rocq-runtime.plugins.ltac2" "mem_constant_transparent_state".
+
+(** [mem_proj p t] checks whether the primitive projection [p] is present in the
+    transparency state [t]. *)
+Ltac2 @ external mem_proj : projection -> t -> bool :=
+  "rocq-runtime.plugins.ltac2" "mem_proj_transparent_state".
+
+(** [mem_var v t] checks whether the local variable [v] is present in the
+    transparency state [t]. *)
+Ltac2 @ external mem_var : ident -> t -> bool :=
+  "rocq-runtime.plugins.ltac2" "mem_var_transparent_state".