diff options
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 1 |
1 files changed, 1 insertions, 0 deletions
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. |