aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authoremakarov2007-04-16 12:04:53 +0000
committeremakarov2007-04-16 12:04:53 +0000
commitdb90eece6a08b62913da82cca0d6d294bad22288 (patch)
treee8a42fa0eb3467b573bb6fd81cce524d512e37ae /dev
parentb76c8dd6c09463c2772d7c7bece901730285735a (diff)
Removed from headers.hva the code to make index point to the section
labels and not other environment labels (such as enumerate or theorem). This facility was added to Hevea, which is available at http://hevea.inria.fr/distri/unstable/hevea-2007-04-16.tar.gz git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9772 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions