diff options
Diffstat (limited to 'test-suite/ltac2')
| -rw-r--r-- | test-suite/ltac2/constr.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v index 018596ed95..8c06bff056 100644 --- a/test-suite/ltac2/constr.v +++ b/test-suite/ltac2/constr.v @@ -10,3 +10,9 @@ Axiom something : SProp. Ltac2 Eval match (kind '(forall x : something, bool)) with | Prod a c => a | _ => throw Match_failure end. + +From Coq Require Import Int63 PArray. +Open Scope array_scope. +Ltac2 Eval match (kind '([|true|true|])) with + | Array _ _ _ ty => ty + | _ => throw Match_failure end. |