Other bugs with "inversion as" (collision between user-provided names and generated equation names).

4 files changed, 45 insertions, 7 deletions

diff --git a/tactics/inv.ml b/tactics/inv.ml
index 2efaa96b6..081b62b18 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -330,7 +330,7 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
    If it can discriminate then the goal is proved, if not tries to use it as
    a rewrite rule. It erases the clause which is given as input *)
 
-let projectAndApply as_mode thin id eqname names depids =
+let projectAndApply as_mode thin avoid id eqname names depids =
   let subst_hyp l2r id =
     tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
       (if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
@@ -352,7 +352,7 @@ let projectAndApply as_mode thin id eqname names depids =
       [if as_mode then clear [id] else tclIDTAC;
        (tclMAP_i (false,false) neqns (function (idopt,_) ->
 	 tclTRY (tclTHEN
-	   (intro_move idopt MoveLast)
+	   (intro_move_avoid idopt avoid MoveLast)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
 	   (tclTRY (onLastHypId (substHypIfVariable (fun id -> subst_hyp false id))))))
@@ -382,6 +382,7 @@ let rewrite_equations as_mode othin neqns names ba =
   Proofview.Goal.nf_enter begin fun gl ->
   let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
   let first_eq = ref MoveLast in
+  let avoid = if as_mode then List.map pi1 nodepids else [] in
   match othin with
     | Some thin ->
         tclTHENLIST
@@ -392,12 +393,13 @@ let rewrite_equations as_mode othin neqns names ba =
              (nLastDecls neqns (fun ctx -> clear (ids_of_named_context ctx)));
 	     tclMAP_i (true,false) neqns (fun (idopt,names) ->
                (tclTHEN
-		 (intro_move idopt MoveLast)
+		 (intro_move_avoid idopt avoid MoveLast)
 		 (onLastHypId (fun id ->
-		   tclTRY (projectAndApply as_mode thin id first_eq names depids)))))
+		   tclTRY (projectAndApply as_mode thin avoid id first_eq names depids)))))
 	       names;
 	     tclMAP (fun (id,_,_) -> tclIDTAC >>= fun () -> (* delay for [first_eq]. *)
-	       intro_move None (if thin then MoveLast else !first_eq))
+               let idopt = if as_mode then Some id else None in
+	       intro_move idopt (if thin then MoveLast else !first_eq))
 	       nodepids;
 	     (tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids)]
     | None ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c5486ce53..ca1e25fbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -604,10 +604,12 @@ let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
 let intro_then_force = intro_then_gen (NamingAvoid []) MoveLast true false
 
-let intro_move idopt hto = match idopt with
-  | None -> intro_gen (NamingAvoid []) hto true false
+let intro_move_avoid idopt avoid hto = match idopt with
+  | None -> intro_gen (NamingAvoid avoid) hto true false
   | Some id -> intro_gen (NamingMustBe (dloc,id)) hto true false
 
+let intro_move idopt hto = intro_move_avoid idopt [] hto
+
 (**** Multiple introduction tactics ****)
 
 let rec intros_using = function
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a9434d6ae..d6e648b9b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -57,6 +57,7 @@ val find_intro_names : rel_context -> goal sigma -> Id.t list
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic
 val intro_move        : Id.t option -> Id.t move_location -> unit Proofview.tactic
+val intro_move_avoid  : Id.t option -> Id.t list -> Id.t move_location -> unit Proofview.tactic
 
   (** [intro_avoiding idl] acts as intro but prevents the new Id.t
      to belong to [idl] *)
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 892dd6d48..850f09434 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -156,3 +156,36 @@ intros * Hyp.
 inversion Hyp as (a,b,H,c,(H1_1,H1_2),(H2_1,H2_2,H2_3)).
 reflexivity.
 Qed.
+
+(* Up to September 2014, Mapp below was called MApp0 because of a bug
+   in intro_replacing (short version of bug 2164.v)
+   (example taken from CoLoR) *)
+
+Parameter Term : Type.
+Parameter isApp : Term -> Prop.
+Parameter appBodyL : forall M, isApp M -> Prop.
+Parameter lower : forall M Mapp, appBodyL M Mapp -> Term.
+
+Inductive BetaStep : Term -> Term -> Prop :=
+  Beta M Mapp Mabs : BetaStep M (lower M Mapp Mabs).
+
+Goal forall M N, BetaStep M N -> True.
+intros M N H.
+inversion H as (P,Mapp,Mabs,H0,H1).
+clear Mapp Mabs H0 H1.
+exact Logic.I.
+Qed.
+
+(* Up to September 2014, H0 below was renamed called H1 because of a collision
+   with the automaticallly generated names for equations.
+   (example taken from CoLoR) *)
+
+Inductive term := Var | Fun : term -> term -> term.
+Inductive lt : term -> term -> Prop :=
+  mpo f g ss ts : lt Var (Fun f ts) -> lt (Fun f ss) (Fun g ts).
+
+Goal forall f g ss ts, lt (Fun f ss) (Fun g ts) -> lt Var (Fun f ts).
+intros.
+inversion H as (f',g',ss',ts',H0).
+exact H0.
+Qed.