diff options
| author |  coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-30 09:53:31 +0000 |
|---|---|---|
| committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-30 09:53:31 +0000 |
| commit | bb6e15cb3d64f2902f98d01b8fe12948a7191095 (patch) | |
| tree | cbc0a0f8e740505fb14d13daa47a30070ff258ea /doc/RefMan-tacex.tex | |
| parent | c15a7826ecaa05bb36e934237b479c7ab2136037 (diff) | |
modif generales claude
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8455 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/RefMan-tacex.tex')
| -rw-r--r-- | doc/RefMan-tacex.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-tacex.tex b/doc/RefMan-tacex.tex index 7a411e822..def17e717 100644 --- a/doc/RefMan-tacex.tex +++ b/doc/RefMan-tacex.tex @@ -807,7 +807,7 @@ is undecidable in general case, don't expect miracles from it! \SeeAlso comments of source file \texttt{tactics/contrib/polynom/quote.ml} -\SeeAlso the tactic \texttt{ring} (chapter \ref{ring}) +\SeeAlso the \texttt{ring} tactic (Chapter~\ref{ring}) \section{Using the tactical language} |