Merge PR #10784: Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kind

Reviewed-by: ppedrot

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
new file mode 100644
index 0000000000..39601d99a8
--- /dev/null
+++ b/test-suite/ltac2/constr.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
+Import Unsafe.
+
+Ltac2 Eval match (kind '(nat -> bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.
+
+Set Allow StrictProp.
+Axiom something : SProp.
+Ltac2 Eval match (kind '(forall x : something, bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.