Fixing inversion after having fixed intros_replacing

in69665dd2480d364162933972de7ffa955eccab4d. There are still situations
when "as" is not given where equations coming from injection are not
yet removed, making invalid the computation of dependencies, what
prevents an hypothesis to be cleared and replaced.

3 files changed, 26 insertions, 5 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5d49a9047..2efaa96b6 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -267,13 +267,14 @@ Summary: nine useless hypotheses!
 Nota: with Inversion_clear, only four useless hypotheses
 *)
 
-let generalizeRewriteIntros tac depids id =
+let generalizeRewriteIntros as_mode tac depids id =
   Proofview.Goal.nf_enter begin fun gl ->
   let dids = dependent_hyps id depids gl in
+  let reintros = if as_mode then intros_replacing else intros_possibly_replacing in
   (tclTHENLIST
     [bring_hyps dids; tac;
      (* may actually fail to replace if dependent in a previous eq *)
-     intros_replacing (ids_of_named_context dids)])
+     reintros (ids_of_named_context dids)])
   end
 
 let error_too_many_names pats =
@@ -340,12 +341,13 @@ let projectAndApply as_mode thin id eqname names depids =
     let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
     let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
     match (kind_of_term t1, kind_of_term t2) with
-    | Var id1, _ -> generalizeRewriteIntros (subst_hyp true id) depids id1
-    | _, Var id2 -> generalizeRewriteIntros (subst_hyp false id) depids id2
+    | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
+    | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2
     | _ -> tac id
     end
   in
-  let deq_trailer id _ _ neqns =
+  let deq_trailer id clear_flag _ neqns =
+    assert (clear_flag == None);
     tclTHENLIST
       [if as_mode then clear [id] else tclIDTAC;
        (tclMAP_i (false,false) neqns (function (idopt,_) ->
@@ -356,6 +358,9 @@ let projectAndApply as_mode thin id eqname names depids =
 	   (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
 	 names);
        (if as_mode then tclIDTAC else clear [id])]
+          (* Doing the above late breaks the computation of dids in 
+             generalizeRewriteIntros, and hence breaks proper intros_replacing
+             but it is needed for compatibility *)
   in
   substHypIfVariable
     (* If no immediate variable in the equation, try to decompose it *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3cd6eb288..83a8c2a49 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -596,6 +596,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
 let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
 let intro_mustbe_force id = intro_gen (NamingMustBe (dloc,id)) MoveLast true false
 let intro_using id = intro_gen (NamingBasedOn (id,[])) MoveLast false false
+
 let intro_then = intro_then_gen (NamingAvoid []) MoveLast false false
 let intro = intro_gen (NamingAvoid []) MoveLast false false
 let introf = intro_gen (NamingAvoid []) MoveLast true false
@@ -653,6 +654,20 @@ let intro_replacing id gl =
    reintroduce y, y,' y''. Note that we have to clear y, y' and y''
    before introducing y because y' or y'' can e.g. depend on old y. *)
 
+(* This version assumes that replacement is actually possible *)
+let intros_possibly_replacing ids =
+  Proofview.Goal.enter begin fun gl ->
+    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let posl = List.fold_right (fun id posl ->
+      (id,get_next_hyp_position id posl hyps) :: posl) ids [] in
+    Tacticals.New.tclTHEN
+      (Tacticals.New.tclMAP (fun id -> Tacticals.New.tclTRY (Proofview.V82.tactic (thin_for_replacing [id]))) ids)
+      (Tacticals.New.tclMAP (fun (id,pos) ->
+        Tacticals.New.tclORELSE (intro_move (Some id) pos) (intro_using id))
+         posl)
+  end
+
+(* This version assumes that replacement is actually possible *)
 let intros_replacing ids =
   Proofview.Goal.enter begin fun gl ->
     let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 349e828a1..a9434d6ae 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -68,6 +68,7 @@ val intro_mustbe_force   : Id.t -> unit Proofview.tactic
 val intro_then           : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
 val intros_using         : Id.t list -> unit Proofview.tactic
 val intros_replacing     : Id.t list -> unit Proofview.tactic
+val intros_possibly_replacing : Id.t list -> unit Proofview.tactic
 
 val intros               : unit Proofview.tactic