blob: 018596ed958f478b963e74017d04d13fecaf2111 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
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.
|
