(* 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. *)