aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorDavid Aspinall1998-10-01 17:27:06 +0000
committerDavid Aspinall1998-10-01 17:27:06 +0000
commit8db7c16234e104960a3d5f09bdf6e8f0572484ba (patch)
treedfebfe958891e2fa422050d51cc548e8b757b080 /doc
parentce6a7a3b011b068f62ba652258aef6393344c65c (diff)
Fixed for new header in coqtags.
Diffstat (limited to 'doc')
0 files changed, 0 insertions, 0 deletions