Merge PR #17894: Add Ltac2.Constr.{is_float,is_uint63,is_array}

Reviewed-by: ppedrot
Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

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).

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.