Merge PR #6728: Extrude monomorphic universe contexts from with Definition constraints.

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 0000000000..bbf72a7648
--- /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).