diff options
| author | bertot | 2001-04-04 12:54:07 +0000 |
|---|---|---|
| committer | bertot | 2001-04-04 12:54:07 +0000 |
| commit | d7121ac57d10609aeb58fd84db4be8038c3247cf (patch) | |
| tree | 964446ce566bf357d4c400ae6f7822c1e812096a /toplevel | |
| parent | f5ed5175d4ae3d70c395839650c0dce77d4ed8f6 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 |