aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorMaxime Dénès2018-09-11 18:35:21 +0200
committerMaxime Dénès2018-09-18 08:36:41 +0200
commit6ab397f8dd3f453d58e2167ca21a9f07aeb2a0c3 (patch)
treeaa9e00f6c21d0f86e6252b2bf5e69b77f1ed06ca /dev
parentf1482433ff225831d9937753f946cff2577b9309 (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