From d14635b0c74012e464aad9e77aeeffda0f1ef154 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Jun 2010 13:56:14 +0000
Subject: Made option "Automatic Introduction" active by default before too
 many people use the undocumented "Lemma foo x : t" feature in a way
 incompatible with this activation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Wf.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 7179135726..3816c15050 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -134,7 +134,6 @@ Section Fix_rects.
             Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
     : forall x a, Q _ (Fix_F_sub A R P f x a).
   Proof with auto.
-    intros Q inv.
     set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)).
     cut (forall x, R' x)...
     apply (well_founded_induction_type Rwf).
@@ -167,7 +166,7 @@ Section Fix_rects.
     Fix_F_sub A R P f x a =
     Fix_F_sub A R P f x a'.
   Proof.
-    intros x a.
+    revert a'.
     pattern x, (Fix_F_sub A R P f x a).
     apply Fix_F_sub_rect.
     intros.
-- 
cgit v1.2.3