From a4aa6a3442ef0bb19ff0da11fe0a20743944aed9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 20 Oct 2009 20:00:26 +0000
Subject: Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12404 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tacex.tex | 1 +
 1 file changed, 1 insertion(+)

diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 306e52ebdd..ec7c9c0b1b 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -866,6 +866,7 @@ rewritings and shows how to deal with them using the optional tactic of the
 %Here is a basic use of {\tt AutoRewrite} with the Ackermann function:
 
 \begin{coq_example*}
+Reset Initial.
 Require Import Arith.
 Variable Ack : 
            nat -> nat -> nat.
-- 
cgit v1.2.3