From c5c5cf0249dd169ea937bd825705829bf9386300 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 26 Jul 2023 13:14:36 -0700
Subject: [PATCH] Add `Ltac2.Constr.{is_float,is_uint63,is_array}`

---
 .../06-Ltac2-language/17894-is_float.rst       |  4 ++++
 user-contrib/Ltac2/Constr.v                    | 18 ++++++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 doc/changelog/06-Ltac2-language/17894-is_float.rst

diff --git a/doc/changelog/06-Ltac2-language/17894-is_float.rst b/doc/changelog/06-Ltac2-language/17894-is_float.rst
new file mode 100644
index 000000000000..fe10bb89e737
--- /dev/null
+++ b/doc/changelog/06-Ltac2-language/17894-is_float.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  ``Ltac2.Constr.is_float``, ``Ltac2.Constr.is_uint63``, ``Ltac2.Constr.is_array``
+  (`#17894 <https://github.com/coq/coq/pull/17894>`_,
+  by Jason Gross).
diff --git a/user-contrib/Ltac2/Constr.v b/user-contrib/Ltac2/Constr.v
index 451b2d91c460..df6a4af8ef1a 100644
--- a/user-contrib/Ltac2/Constr.v
+++ b/user-contrib/Ltac2/Constr.v
@@ -190,3 +190,21 @@ Ltac2 is_const(c: constr) :=
   | Unsafe.Constant _ _ => true
   | _ => false
   end.
+
+Ltac2 is_float(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Float _ => true
+  | _ => false
+  end.
+
+Ltac2 is_uint63(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Uint63 _ => true
+  | _ => false
+  end.
+
+Ltac2 is_array(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Array _ _ _ _ => true
+  | _ => false
+  end.