aboutsummaryrefslogtreecommitdiff
path: root/doc/RefMan-ltac.tex
diff options
context:
space:
mode:
authorfilliatr2001-04-06 14:19:31 +0000
committerfilliatr2001-04-06 14:19:31 +0000
commite1472ba5916efafe186ebe73ca19c4f137b9e890 (patch)
tree6b24b527637547224a225e6a2213e597c329721c /doc/RefMan-ltac.tex
parent48aff2bc219295950c032ba09b748f0690f5a2bc (diff)
mise a jour V7
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8169 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-ltac.tex')
-rw-r--r--doc/RefMan-ltac.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-ltac.tex b/doc/RefMan-ltac.tex
index c2ee955a61..55d2790d8c 100644
--- a/doc/RefMan-ltac.tex
+++ b/doc/RefMan-ltac.tex
@@ -1,4 +1,4 @@
\chapter{The tactic language}
-\label{WritingTactics}
+\label{TacticLanguage}
**TO DO** \ No newline at end of file