diff options
Diffstat (limited to 'doc/Recursive-Definition.tex')
| -rwxr-xr-x | doc/Recursive-Definition.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/Recursive-Definition.tex b/doc/Recursive-Definition.tex index 77774d9fa..6da37204f 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 |