From 1e4ac27962aaab5132c9294156ac2a0da9652a43 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Tue, 2 Oct 2018 14:06:10 +0000
Subject: test-suite: cleaning

---
 test-suite/modules/WithDefUBinders.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'test-suite/modules/WithDefUBinders.v')

diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v
index e683455162..00a93b5fdf 100644
--- a/test-suite/modules/WithDefUBinders.v
+++ b/test-suite/modules/WithDefUBinders.v
@@ -13,3 +13,5 @@ Fail Module M' : T with Definition foo := Type.
 (* Without the binder expression we have to do trickery to get the
    universes in the right order. *)
 Module M' : T with Definition foo := let t := Type in t.
+Definition foo := let t := Type in t.
+End M'.
-- 
cgit v1.2.3