diff options
| author | emakarov | 2007-04-16 12:04:53 +0000 |
|---|---|---|
| committer | emakarov | 2007-04-16 12:04:53 +0000 |
| commit | db90eece6a08b62913da82cca0d6d294bad22288 (patch) | |
| tree | e8a42fa0eb3467b573bb6fd81cce524d512e37ae /dev/include | |
| parent | b76c8dd6c09463c2772d7c7bece901730285735a (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/include')
0 files changed, 0 insertions, 0 deletions