aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Reference-Manual.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
-rw-r--r--doc/refman/Reference-Manual.tex1
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index a6a3670bd..5122b2a36 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -95,7 +95,6 @@ Options A and B of the licence are {\em not} elected.}
\defaultheaders
%END LATEX
\include{RefMan-gal.v}% Gallina
-\include{RefMan-lib.v}% The coq library
\part{The proof engine}