diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-11 22:03:51 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-11 22:03:51 +0000 |
| commit | 20f453081d070752de87d0a1003505288b7a868e (patch) | |
| tree | 72d2e15f9b8d40b24384b71bf1a6b8134c728276 /coq/ex-module.v | |
| parent | 7115f719eafad7d56d7f77a024b9d54d7f3bf07d (diff) | |
Remove deliberately buggy code at the end (Coq seems to be fixed)
Diffstat (limited to 'coq/ex-module.v')
| -rw-r--r-- | coq/ex-module.v | 8 |
1 files changed, 0 insertions, 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. |