aboutsummaryrefslogtreecommitdiff
path: root/test-suite/modules/SeveralWith.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/modules/SeveralWith.v')
-rw-r--r--test-suite/modules/SeveralWith.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/modules/SeveralWith.v b/test-suite/modules/SeveralWith.v
index bbf72a7648..4426f2710a 100644
--- a/test-suite/modules/SeveralWith.v
+++ b/test-suite/modules/SeveralWith.v
@@ -10,3 +10,4 @@ End ES.
Module Make
(AX : S)
(X : ES with Definition A := AX.A with Definition eq := @eq AX.A).
+End Make.