diff options
Diffstat (limited to 'ide/coqidetop.mllib')
| -rw-r--r-- | ide/coqidetop.mllib | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib deleted file mode 100644 index df988d8f..00000000 --- a/ide/coqidetop.mllib +++ /dev/null @@ -1,8 +0,0 @@ -Xml_lexer -Xml_parser -Xml_printer -Serialize -Richpp -Xmlprotocol -Document -Ide_slave |