From a48e965ab8900eef3d08d6ae814b03bce2df431e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 22 Jan 2009 14:47:28 +0000
Subject: Fixes in the documentation of [dependent induction] and test-suite
 scripts.

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

(limited to 'doc')

diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 5da43ec0bb..dbd8634696 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -812,8 +812,7 @@ Require Import Coq.Program.Tactics.
 Lemma weakening : forall G D tau, term (G ; D) tau -> 
   forall tau', term (G , tau' ; D) tau.
 Proof with simpl in * ; simpl_depind ; auto.
-  intros G D tau H.
-  dependent induction H generalizing G D.
+  intros G D tau H. dependent induction H generalizing G D ; intros.
 \end{coq_example*}
 
 This call to \depind has an additional arguments which is a list of
@@ -845,8 +844,8 @@ Show.
   specialize (IHterm G empty).
 \end{coq_example}
 
-Then the automation can find that the needed equality {\tt G = G} to
-narrow the induction hypothesis further. This concludes our example.
+Then the automation can find the needed equality {\tt G = G} to narrow
+the induction hypothesis further. This concludes our example.
 
 \begin{coq_example}
   simpl_depind.
-- 
cgit v1.2.3