1 files changed, 30 insertions, 16 deletions

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index c2cd9e47..4fb76bb8 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -104,22 +104,29 @@ let mkGenDecideEqGoal rectype g =
         (mkDecideEqGoal true (build_coq_sumbool ())
           rectype (mkVar xname) (mkVar yname))))
 
+let rec rewrite_and_clear hyps = match hyps with
+| [] -> Proofview.tclUNIT ()
+| id :: hyps ->
+  tclTHENLIST [
+    Equality.rewriteLR (mkVar id);
+    clear [id];
+    rewrite_and_clear hyps;
+  ]
+
 let eqCase tac =
-  (tclTHEN intro
-  (tclTHEN (onLastHyp Equality.rewriteLR)
-  (tclTHEN clear_last
-  tac)))
+  tclTHEN intro (onLastHypId tac)
 
-let diseqCase eqonleft =
+let diseqCase hyps eqonleft =
   let diseq  = Id.of_string "diseq" in
   let absurd = Id.of_string "absurd" in
   (tclTHEN (intro_using diseq)
   (tclTHEN (choose_noteq eqonleft)
+  (tclTHEN (rewrite_and_clear (List.rev hyps))
   (tclTHEN  (Proofview.V82.tactic red_in_concl)
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (Simple.apply (mkVar diseq))
   (tclTHEN  (Extratactics.injHyp absurd)
-            (full_trivial [])))))))
+            (full_trivial []))))))))
 
 open Proofview.Notations
 
@@ -131,15 +138,24 @@ let match_eqdec c =
 
 (* /spiwack *)
 
-let solveArg eqonleft op a1 a2 tac =
+let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with
+| [], [] ->
+  tclTHENLIST [
+    choose_eq eqonleft;
+    rewrite_and_clear (List.rev hyps);
+    intros_reflexivity;
+  ]
+| a1 :: largs, a2 :: rargs ->
   Proofview.Goal.enter begin fun gl ->
-  let rectype = pf_type_of gl a1 in
+  let rectype = pf_unsafe_type_of gl a1 in
   let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
+  let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in
   let subtacs =
-    if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto]
-    else [diseqCase eqonleft;eqCase tac;default_auto] in
+    if eqonleft then [eqCase tac;diseqCase hyps eqonleft;default_auto]
+    else [diseqCase hyps eqonleft;eqCase tac;default_auto] in
   (tclTHENS (elim_type decide) subtacs)
   end
+| _ -> invalid_arg "List.fold_right2"
 
 let solveEqBranch rectype =
   Proofview.tclORELSE
@@ -152,13 +168,11 @@ let solveEqBranch rectype =
           let getargs l = List.skipn nparams (snd (decompose_app l)) in
           let rargs   = getargs rhs
           and largs   = getargs lhs in
-          List.fold_right2
-            (solveArg eqonleft op) largs rargs
-            (tclTHEN (choose_eq eqonleft) intros_reflexivity)
+          solveArg [] eqonleft op largs rargs
       end
     end
     begin function (e, info) -> match e with
-      | PatternMatchingFailure -> Proofview.tclZERO (UserError ("",Pp.str"Unexpected conclusion!"))
+      | PatternMatchingFailure -> Tacticals.New.tclZEROMSG (Pp.str"Unexpected conclusion!")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -186,7 +200,7 @@ let decideGralEquality =
     end
     begin function (e, info) -> match e with
       | PatternMatchingFailure ->
-          Proofview.tclZERO (UserError ("", Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}."))
+          Tacticals.New.tclZEROMSG (Pp.str"The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}.")
       | e -> Proofview.tclZERO ~info e
     end
 
@@ -203,7 +217,7 @@ let decideEquality rectype =
 
 let compare c1 c2 =
   Proofview.Goal.enter begin fun gl ->
-  let rectype = pf_type_of gl c1 in
+  let rectype = pf_unsafe_type_of gl c1 in
   let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
   (tclTHENS (cut decide)
             [(tclTHEN  intro