Bug calcul du nom de la premiere equation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4601 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 8 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 9f2691b06..0ffe21067 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -288,13 +288,13 @@ let generalizeRewriteIntros tac depids id gls =
   gls
 
 let rec tclMAP_i n tacfun = function
-  | [] -> 
-      if n>0 then tclDO n (tacfun None)
-      else tclIDTAC
+  | [] -> tclDO n (tacfun None)
   | a::l -> 
       if n=0 then error "Too much names"
       else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l)
 
+let remember_first_eq id x = if !x = None then x := Some id
+
 (* invariant: ProjectAndApply is responsible for erasing the clause
    which it is given as input
    It simplifies the clause (an equality) to use it as a rewrite rule and then
@@ -305,16 +305,17 @@ let rec tclMAP_i n tacfun = function
 
 let projectAndApply thin id eqname names depids gls =
   let env = pf_env gls in
-  let clearer = if thin then clear else fun _ -> tclIDTAC in
-  let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id None)) (clearer [id]) in
-  let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id None)) (clearer [id]) in
+  let clearer id =
+    if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC) in
+  let subst_hyp_LR id = tclTHEN (tclTRY(hypSubst_LR id None)) (clearer id) in
+  let subst_hyp_RL id = tclTHEN (tclTRY(hypSubst_RL id None)) (clearer id) in
   let substHypIfVariable tac id gls =
-    eqname := Some id; (* remember where to re-intro hyps later *)
     let (t,t1,t2) = Hipattern.dest_nf_eq gls (pf_get_hyp_typ gls id) in
     match (kind_of_term t1, kind_of_term t2) with
       | Var id1, _ -> generalizeRewriteIntros (subst_hyp_LR id) depids id1 gls
       | _, Var id2 -> generalizeRewriteIntros (subst_hyp_RL id) depids id2 gls
-      | _ -> 
+      | _ ->
+	  
 	  tac id gls
   in
   let deq_trailer id neqns =