From 20f453081d070752de87d0a1003505288b7a868e Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 11 Aug 2010 22:03:51 +0000
Subject: Remove deliberately buggy code at the end (Coq seems to be fixed)

---
 coq/ex-module.v | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/coq/ex-module.v b/coq/ex-module.v
index e6e3511f..7e75f59b 100644
--- a/coq/ex-module.v
+++ b/coq/ex-module.v
@@ -90,11 +90,3 @@ Lemma titi : O=O.
   Module Type K:=N'.
   Module N''':=M.
 Save.
-
-	 (* Here is a bug of Coq: *)
-
-Lemma bar:O=O.
-  Module Type L. (* This should not be allowed by Coq, since the End L. below fails *)
-End L. (* fails --> if we go back to Module Type: unsync *)
-Module I.
-End I.
-- 
cgit v1.2.3