diff options
| author | Enrico Tassi | 2018-03-21 18:11:13 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-03-21 18:11:13 +0100 |
| commit | f08dfceda3930bdd42602490a6ad4174db509702 (patch) | |
| tree | 1bc7263be2c770856ff3c17513e812b26d65acb2 /printing/printer.ml | |
| parent | d7ea089b890e93d42c9b3ddb3b521590f73356bc (diff) | |
Remove obsolete files from dev/doc
- cic.dtd is related to the XML plugin
- about-hints uses v7 syntax
- minicoq.tex talks about a tool that is not there
- translate.txt talks about the v7->v8 translation machinery
- transition-* talk about v5->v7 changes to the sources layout
Diffstat (limited to 'printing/printer.ml')
0 files changed, 0 insertions, 0 deletions