Continuing r16621 on injection intro-patterns:

- order of hypothesis was (historically) from right to left in injection but
  already from left to right in decomp_eq, so no need ro fix it there
- made test Injection.v consistent with implementation

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

2 files changed, 7 insertions, 7 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 20e7f2b2ce..b991defe73 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1214,7 +1214,7 @@ let injClause ipats with_evars = function
 let injConcl gls  = injClause None false None gls
 let injHyp id gls = injClause None false (Some (ElimOnIdent (Loc.ghost,id))) gls
 
-let decompEqThen ntac l2r (lbeq,_,(t,t1,t2) as u) clause gls =
+let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause gls =
   let sort = pf_apply get_type_of gls (pf_concl gls) in
   let sigma = clause.evd in
   let env = pf_env gls in
@@ -1224,16 +1224,16 @@ let decompEqThen ntac l2r (lbeq,_,(t,t1,t2) as u) clause gls =
     | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
         ntac (clenv_value clause) 0 gls
     | Inr posns ->
-	inject_at_positions env sigma l2r u clause (List.rev posns)
+	inject_at_positions env sigma true u clause posns
           (ntac (clenv_value clause)) gls
 
 let dEqThen with_evars ntac = function
-  | None -> onNegatedEquality with_evars (decompEqThen ntac false)
-  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac false)) c
+  | None -> onNegatedEquality with_evars (decompEqThen ntac)
+  | Some c -> onInductionArg (onEquality with_evars (decompEqThen ntac)) c
 
 let dEq with_evars = dEqThen with_evars (fun c x -> tclIDTAC)
 
-let _ = declare_intro_decomp_eq (fun tac -> decompEqThen (fun _ -> tac) true)
+let _ = declare_intro_decomp_eq (fun tac -> decompEqThen (fun _ -> tac))
 
 let swap_equality_args = function
   | MonomorphicLeibnizEq (e1,e2) -> [e2;e1]
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index f1ee8a05f7..9d5047fdc3 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -39,7 +39,7 @@ Qed.
 (* Test injection as *)
 
 Lemma l5 : forall x y z t : nat, (x,y) = (z,t) -> x=z.
-intros; injection H as Hyt Hxz.
+intros; injection H as Hxz Hyt.
 exact Hxz.
 Qed.
 
@@ -69,7 +69,7 @@ Abort.
 (* Test the injection intropattern *)
 
 Goal forall (a b:nat) l l', cons a l = cons b l' -> a=b.
-intros * (H1,H2).
+intros * [= H1 H2].
 exact H1.
 Qed.