version et style

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8371 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/Recursive-Definition.tex b/doc/Recursive-Definition.tex
index 77774d9fa0..6da37204fa 100755
--- a/doc/Recursive-Definition.tex
+++ b/doc/Recursive-Definition.tex
@@ -2,7 +2,7 @@
 \input{title}
 
 \newcommand{\xx}{\noindent}
-\newcommand{\Coq}{{\sf Coq}}
+\newcommand{\Coq}{\textsc{Coq}}
 
 \begin{document}
 
@@ -101,13 +101,13 @@ function.
 \xx
 Such a proof is {\em automatically} synthesized by a
 {specialized strategy} which was originally designed for the
-{\sf ProPre} programming language. It has been adapted for
-the \Coq's framework. For a short description of the {\sf
-ProPre} programming language, we refer the reader to
+\textsc{ProPre} programming language. It has been adapted for
+the \Coq's framework. For a short description of the \textsc{ProPre}
+programming language, we refer the reader to 
 \cite{MPSI}. For details 
 concerning the original proof search strategy, we refer the
 reader to \cite{MSAR}. For theoretical settings of the
-method involved in {\sf ProPre}, we refer the reader to
+method involved in \textsc{ProPre}, we refer the reader to
 \cite{KRPA} and \cite{PARI}.
 
 \xx