From 35a743761478fffaaafd54368a5dcbcecd3133eb Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 30 Jul 2015 09:53:30 +0200
Subject: Fix some broken Coq scripts in the documentation.

---
 doc/refman/Program.tex | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'doc/refman/Program.tex')

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.
 
-- 
cgit v1.2.3