From 0f281377613d77752289f5d9ce100a25d724df61 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 10 Jul 2013 09:24:37 +0000
Subject: 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
---
 tactics/equality.ml            | 10 +++++-----
 test-suite/success/Injection.v |  4 ++--
 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.
 
-- 
cgit v1.2.3