diff options
| -rw-r--r-- | test-suite/ltac2/syntax.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/ltac2/syntax.v b/test-suite/ltac2/syntax.v new file mode 100644 index 0000000000..872b2142d0 --- /dev/null +++ b/test-suite/ltac2/syntax.v @@ -0,0 +1,12 @@ +Require Import Ltac2.Ltac2. + +Ltac2 Type ('a, 'b, 'c) t. +Ltac2 Type ('a) u. +Ltac2 Type 'a v. + +Ltac2 foo + (f : ('a, 'b, 'c) t -> ('a -> 'a, 'b -> 'c, 'c * 'c) t) + (x : ('a, 'b, 'c) t) := + f x. + +Ltac2 bar (x : 'a u) (y : ('b) v) := x. |