From d7121ac57d10609aeb58fd84db4be8038c3247cf Mon Sep 17 00:00:00 2001
From: bertot
Date: Wed, 4 Apr 2001 12:54:07 +0000
Subject: Add a Comments command, that does nothing, but is quite useful to to
 have well displayed comments in the middle of developments (that is comments
 that are more than just plain strings).  Used in the graphical interface
 pcoq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1537 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c7b68ecea6..d56b566025 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -402,6 +402,8 @@ let _ =
        | [] -> (fun () -> ())
        | _  -> bad_vernac_args "GOAL")
 
+let _ = add "Comments" (function _ -> (fun () -> ()))
+
 let _ =
   add "ABORT"
     (function 
-- 
cgit v1.2.3