diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:28 -0500 |
| commit | 1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch) | |
| tree | 5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /dev/doc/coq-src-description.txt | |
| parent | 3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff) | |
| parent | 9ebf44d84754adc5b64fcf612c6816c02c80462d (diff) | |
Updated version 8.9.0 from 'upstream/8.9.0'
with Debian dir 81a4f85bc45e59aa1eadb4797f0eb0b8039efb63
Diffstat (limited to 'dev/doc/coq-src-description.txt')
| -rw-r--r-- | dev/doc/coq-src-description.txt | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index b3d49b7e..764d4829 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -17,12 +17,6 @@ toplevel Special components ------------------ -intf : - - Contains mli-only interfaces, many of them providing a.s.t. - used for dialog bewteen coq components. Ex: Constrexpr.constr_expr - produced by parsing and transformed by interp. - grammar : Camlp5 syntax extensions. The file grammar/grammar.cma is used |