summaryrefslogtreecommitdiff
path: root/doc/refman/Reference-Manual.tex
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-07-13 14:28:31 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-07-13 14:28:31 +0000
commitde0085539583f59dc7c4bf4e272e18711d565466 (patch)
tree347e1d95a2df56f79a01b303e485563588179e91 /doc/refman/Reference-Manual.tex
parente978da8c41d8a3c19a29036d9c569fbe2a4616b0 (diff)
Imported Upstream version 8.0pl3+8.1beta.2upstream/8.0pl3+8.1beta.2
Diffstat (limited to 'doc/refman/Reference-Manual.tex')
-rw-r--r--doc/refman/Reference-Manual.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 4542e730..14fbff47 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -68,7 +68,7 @@
\include{RefMan-oth.v}% Vernacular commands
\include{RefMan-pro}% Proof handling
\include{RefMan-tac.v}% Tactics and tacticals
-\include{RefMan-ltac}% Writing tactics
+\include{RefMan-ltac.v}% Writing tactics
\include{RefMan-tacex.v}% Detailed Examples of tactics
\part{User extensions}
@@ -122,4 +122,4 @@
\end{document}
-% $Id: Reference-Manual.tex 8688 2006-04-07 15:08:12Z msozeau $
+% $Id: Reference-Manual.tex 9038 2006-07-11 13:53:53Z herbelin $