diff options
| -rw-r--r-- | etc/coq/nested.v | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/etc/coq/nested.v b/etc/coq/nested.v index ab2af6c6..bd447157 100644 --- a/etc/coq/nested.v +++ b/etc/coq/nested.v @@ -2,7 +2,7 @@ BUGS: - None??? + - Nested sections... ======= Below here fixed @@ -79,7 +79,21 @@ End Apple. Section Banana. Lemma Coq: O=O. Auto. Save. (* silly example to show that testing - prompt to determine if we're in proof - mode is not good enough. *) + prompt in coq-proof-mode-p to determine + if we're in proof mode is not good enough. + Hopefully nobody calls their theorems "Coq".*) End Banana. + +(* Nested sections? + Oh no, this is too horrible to even think about. *) + +Section Cranberry. + + Section Damson. + + Lemma CoqIsStrange: O=O. Auto. Save. + + End Damson. + +End Cranberry. |