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 /kernel/type_errors.ml | |
| 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 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions