etc/coq/parsing.v


1
2
3
4
5
6
7
8
9
10
11

(* Here's a test of a 

  (* nested comment:
	Since Coq has them, PG ought to be able to deal
        with them.  They work fine in GNU Emacs, but
        problematical in XEmacs. *)
*)

Require Logic.

(* Comment at the end here. *)