Merge PR #12594: Fix ltac2 type parameters

Reviewed-by: MSoegtropIMC
Reviewed-by: gares

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.