diff options
author | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-04-24 21:36:59 -0700 |
---|---|---|
committer | Jasper Hugunin <jasperh@cs.washington.edu> | 2018-04-24 21:36:59 -0700 |
commit | ea24fed3a1a91f945d0cce380d0ea1a9156e735e (patch) | |
tree | 69be6177e5bae042f8a70ceaa6aee5e195991f8b /printing/genprint.mli | |
parent | 72d6d5e87759b62dcd9974c87bf59496d27e10b0 (diff) |
Remove DirClosedSection.
This has been around for at least 16 years, with the comment
"this won't last long I hope".
https://github.com/coq/coq/commit/12965209478bd99dfbe57f07d5b525e51b903f22#diff-1a3a6f7bd5b2cf1bc6dd43ee04bbc3eaR112
Diffstat (limited to 'printing/genprint.mli')
0 files changed, 0 insertions, 0 deletions