From e2655d38d11b072da0e5f4d40b05adbea73c8b8d Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 10 Apr 2009 19:23:58 +0000
Subject: Fix premature optimisation in dependent induction: even variable args
 need to be generalized as they may appear in other arguments or their types.
 Try to keep the original names around as well, using the ones found in the
 goal. This only requires that interning a pattern [forall x, _] properly
 declares [x] as a metavariable, binding instances are already part of the
 substitutions computed by [extended_matches].

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

(limited to 'theories/Program')

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index be2f176d37..6c4fe71fcd 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -384,6 +384,7 @@ Ltac simplify_one_dep_elim_term c :=
       intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ;
         case hyp ; clear hyp
     | block_dep_elim ?T => fail 1 (* Do not put any part of the rhs in the hyps *)
+    | forall x, _ => intro x || (let H := fresh x in rename x into H ; intro x) (* Try to keep original names *)
     | _ => intro
   end.
 
@@ -479,9 +480,11 @@ Ltac intro_prototypes :=
     | _ => idtac
   end.
 
-Ltac introduce p := 
-  first [ match p with _ => idtac end (* Already there *)
-    | intros until p | intros ].
+Ltac introduce p := first [ 
+  match p with _ => (* Already there, generalize dependent hyps *) 
+    generalize dependent p ; intros p 
+  end
+  | intros until p | intros ].
 
 Ltac do_case p := introduce p ; (destruct p || elim_case p || (case p ; clear p)).
 Ltac do_ind p := introduce p ; (induction p || elim_ind p).
-- 
cgit v1.2.3