diff options
| author | coq | 2003-12-30 09:53:31 +0000 |
|---|---|---|
| committer | coq | 2003-12-30 09:53:31 +0000 |
| commit | bb6e15cb3d64f2902f98d01b8fe12948a7191095 (patch) | |
| tree | cbc0a0f8e740505fb14d13daa47a30070ff258ea /doc/AddRefMan-pre.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/AddRefMan-pre.tex')
| -rw-r--r-- | doc/AddRefMan-pre.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex index bd661aeefe..29632d67f5 100644 --- a/doc/AddRefMan-pre.tex +++ b/doc/AddRefMan-pre.tex @@ -33,7 +33,7 @@ Manual. % manual of the tools he wrote for printing proofs in natural % language. At this time, French and English languages are supported. -\item[Omega] \texttt{Omega}, written by Pierre Crégut, solves a whole +\item[omega] \texttt{omega}, written by Pierre Crégut, solves a whole class of arithmetic problems. %\item[Program] The \texttt{Program} technology intends to inverse the @@ -41,7 +41,7 @@ Manual. % programs in \Coq. This chapter is due to Catherine Parent. {\bf This % feature is not available in {\Coq} version 7.} -\item[The {\tt Ring} tactic] This is a tactic to do AC rewriting. This +\item[The {\tt ring} tactic] This is a tactic to do AC rewriting. This chapter explains how to use it and how it works. The chapter is contributed by Patrick Loiseleur. |