diff --git a/doc/changelog/06-Ltac2-language/22261-ltac2-constr-is-prod-nd-Added.rst b/doc/changelog/06-Ltac2-language/22261-ltac2-constr-is-prod-nd-Added.rst
new file mode 100644
index 000000000000..bb6794b4bb4c
--- /dev/null
+++ b/doc/changelog/06-Ltac2-language/22261-ltac2-constr-is-prod-nd-Added.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Ltac2 function ``Constr.is_prod_nd``
+  (`#22261 <https://github.com/rocq-prover/rocq/pull/22261>`_,
+  by Jason Gross).
diff --git a/test-suite/ltac2/constr_is_prod_nd.v b/test-suite/ltac2/constr_is_prod_nd.v
new file mode 100644
index 000000000000..032d246a9d0a
--- /dev/null
+++ b/test-suite/ltac2/constr_is_prod_nd.v
@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 Type exn ::= [ Regression_Test_Failure ].
+Ltac2 check (b : bool) := if b then () else Control.throw Regression_Test_Failure.
+
+Ltac2 Eval check (Constr.is_prod_nd constr:(nat -> nat)).
+Ltac2 Eval check (Constr.is_prod_nd constr:(nat -> nat -> bool)).
+Ltac2 Eval check (Bool.neg (Constr.is_prod_nd constr:(forall n : nat, n = n))).
+Ltac2 Eval check (Constr.is_prod_nd constr:(forall _ : nat, nat)).
+Ltac2 Eval check (Bool.neg (Constr.is_prod_nd constr:(fun n : nat => n))).
+Ltac2 Eval check (Bool.neg (Constr.is_prod_nd constr:(0))).
diff --git a/theories/Ltac2/Constr.v b/theories/Ltac2/Constr.v
index bae4c954caa0..0331198a4495 100644
--- a/theories/Ltac2/Constr.v
+++ b/theories/Ltac2/Constr.v
@@ -648,3 +648,11 @@ Ltac2 is_case(c: constr) :=
   | Unsafe.Case _ _ _ _ _ => true
   | _ => false
   end.
+
+(** [is_prod_nd c] returns [true] iff [c] is a non-dependent product,
+    i.e. a product whose codomain does not use the bound variable. *)
+Ltac2 is_prod_nd(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Prod _ body => Unsafe.noccurn 1 body
+  | _ => false
+  end.