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.

6 files changed, 59 insertions, 7 deletions

diff --git a/CHANGES b/CHANGES
index 8fae9fb6f4..c03e30bdfe 100644
--- a/CHANGES
+++ b/CHANGES
@@ -189,6 +189,7 @@ Tactics
   swapped, as a more friendly replacement of "cut".
 - In destruct/induction, experimental modifier "!" prefixing the
   hypothesis name to tell not erasing the hypothesis.
+- Bug fixes in "inversion as" may occasionally lead to incompatibilities.
 
 Program
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 90055ea837..e8ec731e61 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2272,7 +2272,7 @@ several times. See Section~\ref{Derive-Inversion}.
 
 \item \tacindex{inversion \dots\ as} \texttt{inversion {\ident} as \intropattern}
 
-  This behaves as \texttt{inversion} but using names in
+  This generally behaves as \texttt{inversion} but using names in
   {\intropattern} for naming hypotheses. The {\intropattern} must have
   the form {\tt [} $p_{11} \ldots p_{1n_1}$ {\tt |} {\ldots} {\tt |}
   $p_{m1} \ldots p_{mn_m}$ {\tt ]} with $m$ being the number of
@@ -2294,6 +2294,13 @@ several times. See Section~\ref{Derive-Inversion}.
   \dots, $p_{ijq}$)}) where $q$ is the number of subequalities
   obtained from splitting the original equation. Here is an example.
 
+  The \texttt{inversion \dots\ as} variant of \texttt{inversion}
+  generally behaves in a slightly more expectable way than
+  \texttt{inversion} (no artificial duplication of some hypotheses
+  referring to other hypotheses) To take benefit of these
+  improvements, it is enough to use \texttt{inversion \dots\ as []},
+  letting the names being finally chosen by {\Coq}.
+
 \begin{coq_eval}
 Require Import List.
 \end{coq_eval}
@@ -2319,7 +2326,10 @@ Abort.
   {\ident} as \intropattern}
 
   This allows naming the hypotheses introduced by
-  \texttt{inversion\_clear} in the context.
+  \texttt{inversion\_clear} in the context. Notice that hypothesis
+  names can be provided as if \texttt{inversion} were called, even
+  though the \texttt{inversion\_clear} will eventually erase the
+  hypotheses.
 
 \item \tacindex{inversion \dots\ in} \texttt{inversion {\ident}
   in \ident$_1$ \dots\ \ident$_n$}
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 5d49a90473..2efaa96b6d 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 3cd6eb2881..83a8c2a49b 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 349e828a19..a9434d6ae7 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
 
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index b068f7298c..892dd6d489 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -136,3 +136,23 @@ Goal True -> True.
 intro.
 Fail inversion H using False.
 Fail inversion foo using True_ind.
+
+(* Was failing at some time between 7 and 10 September 2014 *)
+(* even though, it is not clear that the resulting context is interesting *)
+
+Parameter P:nat*nat->Prop.
+Inductive IND : nat * nat -> { x : nat * nat | P x } * nat -> Prop :=
+CONSTR a b (H:P (a,b)) c : IND (a,b) (exist _ (a,b) H, c).
+
+Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z.
+intros * Hyp.
+inversion Hyp.
+  (* By the way, why is "H" removed even in non-clear mode ? *)
+reflexivity.
+Qed.
+
+Goal forall x y z t u (H':P (z,t)), IND (x,y) (exist _ (z,t) H', u) -> x = z.
+intros * Hyp.
+inversion Hyp as (a,b,H,c,(H1_1,H1_2),(H2_1,H2_2,H2_3)).
+reflexivity.
+Qed.