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 | |
| 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
| -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 |