Merge PR #20088: Add Ltac2.Constr.{is_string,is_sort}

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

Author: coqbot-app[bot]

doc/changelog/06-Ltac2-language/20088-ltac2-is-sort.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  ``Ltac2.Constr.is_string``, ``Ltac2.Constr.is_sort``
+  (`#20088 <https://github.com/coq/coq/pull/20088>`_,
+  by Jason Gross).

user-contrib/Ltac2/Constr.v

@@ -479,8 +479,20 @@ Ltac2 is_uint63(c: constr) :=
   | _ => false
   end.
 
+Ltac2 is_string(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.String _ => true
+  | _ => false
+  end.
+
 Ltac2 is_array(c: constr) :=
   match Unsafe.kind c with
   | Unsafe.Array _ _ _ _ => true
   | _ => false
   end.
+
+Ltac2 is_sort(c: constr) :=
+  match Unsafe.kind c with
+  | Unsafe.Sort _ => true
+  | _ => false
+  end.