diff options
| -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. |