2 files changed, 7 insertions, 7 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 8172b57714..65b49893b0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1491,10 +1491,10 @@ the local context.
 \tacindex{contradiction}
 
 This tactic applies to any goal. The {\tt contradiction} tactic
-attempts to find in the current context (after all {\tt intros}) one
-hypothesis that is equivalent to {\tt False}. It permits to prune
-irrelevant cases. This tactic is a macro for the tactics sequence
-{\tt intros; elimtype False; assumption}.
+attempts to find in the current context (after all {\tt intros}) an
+hypothesis that is equivalent to an empty inductive type (e.g. {\tt
+  False}), to the negation of a singleton inductive type (e.g. {\tt
+  True} or {\tt x=x}), or two contradictory hypotheses.
 
 \begin{ErrMsgs}
 \item \errindex{No such assumption}
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 10271ce0ca..9962ce9961 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -102,7 +102,7 @@ generator using for instance the command:
 
 This command generates a file \texttt{Makefile} that can be used to
 compile all the sources of the current project. It follows the
-syntax described by the output of \texttt{\% coq\_makefile ----help}.
+syntax described by the output of \texttt{\% coq\_makefile -{}-help}.
 Once the \texttt{Makefile} file has been generated a first time, it
 can be used by the \texttt{make} command to compile part or all of
 the project. Note that once it has been generated once, as soon as
@@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}.
 The following command generates a minimal example of
 \texttt{\_CoqProject} file:
 \begin{quotation}
-\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name
-  '*.v' -print \} > \_CoqProject}
+\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name
+  "*.v" -print ) > \_CoqProject}
 \end{quotation}
 when executed at the root of the directory containing the
 project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files