Fix some broken Coq scripts in the documentation.

1 files changed, 5 insertions, 5 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 76bcaaae67..8e078e9814 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.