From bb6e15cb3d64f2902f98d01b8fe12948a7191095 Mon Sep 17 00:00:00 2001 From: coq Date: Tue, 30 Dec 2003 09:53:31 +0000 Subject: modif generales claude git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8455 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/AddRefMan-pre.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc/AddRefMan-pre.tex') 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. -- cgit v1.2.3