aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/coq-src-description.txt
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/coq-src-description.txt')
-rw-r--r--dev/doc/coq-src-description.txt6
1 files changed, 0 insertions, 6 deletions
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index b3d49b7e5..764d48295 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