1 files changed, 8 insertions, 8 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 76bcaaae67..11dd3a0517 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -42,20 +42,20 @@ operation (see Section~\ref{Caseexpr}).
   generalized by the corresponding equality. As an example,
   the expression: 
 
-\begin{coq_example*}
+\begin{verbatim}
   match x with
   | 0 => t
   | S n => u
   end.
-\end{coq_example*}
+\end{verbatim}
 will be first rewritten to:
-\begin{coq_example*}
+\begin{verbatim}
   (match x as y return (x = y -> _) with
   | 0 => fun H : x = 0 -> t
   | S n => fun H : x = S n -> u
   end) (eq_refl n).
-\end{coq_example*}
-  
+\end{verbatim}
+
   This permits to get the proper equalities in the context of proof
   obligations inside clauses, without which reasoning is very limited.
 
@@ -201,7 +201,7 @@ in their context. In this case, the obligations should be transparent
 recursive calls can be checked by the
 kernel's type-checker. There is an optimization in the generation of
 obligations which gets rid of the hypothesis corresponding to the
-functionnal when it is not necessary, so that the obligation can be
+functional when it is not necessary, so that the obligation can be
 declared opaque (e.g. using {\tt Qed}). However, as soon as it appears in the
 context, the proof of the obligation is \emph{required} to be declared transparent.
 
@@ -216,7 +216,7 @@ properties. It will generate obligations, try to solve them
 automatically and fail if some unsolved obligations remain. 
 In this case, one can first define the lemma's
 statement using {\tt Program Definition} and use it as the goal afterwards.
-Otherwise the proof will be started with the elobarted version as a goal.
+Otherwise the proof will be started with the elaborated version as a goal.
 The {\tt Program} prefix can similarly be used as a prefix for {\tt Variable}, {\tt
   Hypothesis}, {\tt Axiom} etc...
 
@@ -261,7 +261,7 @@ tactic is replaced by the default one if not specified.
   as implicit arguments of the special constant
   \texttt{Program.Tactics.obligation}.
 \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations}
-  Control whether obligations defined by tactics should have their
+  Control whether obligations should have their
   context minimized to the set of variables used in the proof of the
   obligation, to avoid unnecessary dependencies.
 \end{itemize}