blob: 8c06bff0567e0279a6d13f1378b1b1bdb3722d7b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
Import Unsafe.
Ltac2 Eval match (kind '(nat -> bool)) with
| Prod a c => a
| _ => throw Match_failure end.
Set Allow StrictProp.
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.
|
