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

