diff options
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. |