diff options
| author | Pierre-Marie Pédrot | 2020-06-26 09:53:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-01 13:33:08 +0200 |
| commit | 7bec233c0e5ea056c2d8cc5dbfc034b619a9f5dd (patch) | |
| tree | 076cc3ad8c85b0325e2fc5a08fd7cc68c9d8808f | |
| parent | 4e498fa2c96f4217c2d1204ebc032f224f93dbc4 (diff) | |
Add a test for Ltac2 parsing of parameterized types.
| -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. |