Adding a test for the construction that was broken in Coccinelle.

There was no test in the test-suite checking for double with-def constraints
in module typing.

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v
new file mode 100644
index 000000000..bbf72a764
--- /dev/null
+++ b/test-suite/modules/SeveralWith.v
@@ -0,0 +1,12 @@
+Module Type S.
+Parameter A : Type.
+End S.
+
+Module Type ES.
+Parameter A : Type.
+Parameter eq : A -> A -> Type.
+End ES.
+
+Module Make
+  (AX : S)
+  (X : ES with Definition A := AX.A with Definition eq := @eq AX.A).