diff options
| author | Maxime Dénès | 2018-09-11 18:35:21 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-18 08:36:41 +0200 |
| commit | 6ab397f8dd3f453d58e2167ca21a9f07aeb2a0c3 (patch) | |
| tree | aa9e00f6c21d0f86e6252b2bf5e69b77f1ed06ca /dev | |
| parent | f1482433ff225831d9937753f946cff2577b9309 (diff) | |
Removing Dischargedhypsmap which is unused internally.
The Dischargedhypsmap table collected the segment of section variables
that constants defined in a section were originally depending on. It
was useful to reconstruct the structure of sections as originally
given in a source file. In particular this was used in Sacerdoti
Coen's plugin for exportation of Coq files to xml. There is no
information that this plugin, moved out of Coq in September 2014, was
finally maintained, even as an external plugin. So it seems that the
Dischargedhypsmap table is virtually not used anymore in the wild.
Please contact the developers if ever the need for such a table
happens to be necessary for your work.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions
