Fixed a bug in the interaction between dEqThen and inject_at_positions

which was disturbing inversion and sometimes making it failing in
presence of dependent equalities (injection still doesn't know how to
split dependent equalities, resulting in a smaller number of
equalities than expected for dEqThen).
[also restored inv.ml as it was before 12356 which uselessly and
inadvertently modified it]



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

3 files changed, 36 insertions, 16 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f84a0e303..6adfa3aaf 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -920,7 +920,7 @@ let simplify_args env sigma t =
     | eq, [t1;c1;t2;c2] -> applist (eq,[t1;nf env sigma c1;t2;nf env sigma c2])
     | _ -> t
 
-let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns =
+let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns tac =
   let e = next_ident_away eq_baseid (ids_of_context env) in
   let e_env = push_named (e,None,t) env in
   let injectors =
@@ -938,9 +938,11 @@ let inject_at_positions env sigma (eq,_,(t,t1,t2)) eq_clause posns =
       posns in
   if injectors = [] then
     errorlabstrm "Equality.inj" (str "Failed to decompose the equality.");
-  tclMAP
-    (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
-    injectors
+  tclTHEN
+    (tclMAP
+      (fun (pf,ty) -> tclTHENS (cut ty) [tclIDTAC; refine pf])
+      injectors)
+    (tac (List.length injectors))
 
 exception Not_dep_pair
 
@@ -993,9 +995,8 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
 (* not a dep eq or no decidable type found *)
             ) else (raise Not_dep_pair)
         ) with _ ->
-	tclTHEN
-	  (inject_at_positions env sigma u eq_clause posns)
-	  (intros_pattern no_move ipats)
+	  inject_at_positions env sigma u eq_clause posns
+	    (fun _ -> intros_pattern no_move ipats)
 
 let inj ipats with_evars = onEquality with_evars (injEq ipats)
 
@@ -1016,10 +1017,7 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
         ntac 0 gls
     | Inr posns ->
-	tclTHEN
-	  (inject_at_positions env sigma u clause (List.rev posns))
-	  (ntac (List.length posns))
-	  gls
+	inject_at_positions env sigma u clause (List.rev posns) ntac gls
 
 let dEqThen with_evars ntac = function
   | None -> onNegatedEquality with_evars (decompEqThen ntac)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0080f079b..2a11d6520 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -320,11 +320,11 @@ let projectAndApply thin id eqname names depids gls =
     tclTHENSEQ
       [(if names <> [] then clear [id] else tclIDTAC);
        (tclMAP_i neqns (fun idopt ->
-	 tclTHEN
+	 tclTRY (tclTHEN
 	   (intro_move idopt no_move)
 	   (* try again to substitute and if still not a variable after *)
 	   (* decomposition, arbitrarily try to rewrite RL !? *)
-	   (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false)))))
+	   (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false))))))
 	 names);
        (if names = [] then clear [id] else tclIDTAC)]
   in
@@ -406,7 +406,7 @@ let rewrite_equations othin neqns names ba gl =
   let rewrite_eqns =
     let first_eq = ref no_move in
     match othin with
-      | Some thin -> fun gl ->
+      | Some thin ->
           tclTHENSEQ
             [onHyps (compose List.rev (nLastDecls neqns)) bring_hyps;
              onHyps (nLastDecls neqns) (compose clear ids_of_named_context);
@@ -420,11 +420,11 @@ let rewrite_equations othin neqns names ba gl =
 	     tclMAP (fun (id,_,_) gl ->
 	       intro_move None (if thin then no_move else !first_eq) gl)
 	       nodepids;
-	     tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] gl
+	     tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids]
       | None -> tclIDTAC
   in
   (tclTHENSEQ
-    [(fun gl -> tclDO neqns intro gl);
+    [tclDO neqns intro;
      bring_hyps nodepids;
      clear (ids_of_named_context nodepids);
      rewrite_eqns])
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 71e53191b..e8a68c11d 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -107,3 +107,25 @@ Goal forall o, foo2 o -> 0 = 1.
 intros.
 eapply trans_eq.
 inversion H.
+
+(* Check that the part of "injection" that is called by "inversion"
+   does the same number of intros as the number of equations
+   introduced, even in presence of dependent equalities that
+   "injection" renounces to split *)
+
+Fixpoint prodn (n : nat) :=
+  match n with
+  | O => unit 
+  | (S m) => prod (prodn m) nat
+  end.
+
+Inductive U : forall n : nat, prodn n -> bool -> Prop :=
+| U_intro : U 0 tt true.
+
+Lemma foo3 : forall n (t : prodn n), U n t true -> False.
+Proof.
+(* used to fail because dEqThen thought there were 2 new equations but
+   inject_at_positions actually introduced only one; leading then to
+   an inconsistent state that disturbed "inversion" *)
+intros. inversion H.
+Abort.