aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/coq
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-09-11 14:49:00 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-09-11 14:49:00 +0000
commitaa55f69270d2fa9bac16a4950132b6a221374fc1 (patch)
treeda501a69baa7899ad406b44150bf6592cb4aafd3 /etc/coq
parente49408f5b78c2f04aad874b398c257107218eede (diff)
Add comment at end
Diffstat (limited to 'etc/coq')
-rw-r--r--etc/coq/parsing.v8
1 files changed, 5 insertions, 3 deletions
diff --git a/etc/coq/parsing.v b/etc/coq/parsing.v
index 5858922d..be64e62e 100644
--- a/etc/coq/parsing.v
+++ b/etc/coq/parsing.v
@@ -2,8 +2,10 @@
(* nested comment:
Since Coq has them, PG ought to be able to deal
- with them.
- *)
+ with them. They work fine in GNU Emacs, but
+ problematical in XEmacs. *)
*)
-Require Logic. \ No newline at end of file
+Require Logic.
+
+(* Comment at the end here. *)