Merge branch 'v8.5'

2 files changed, 28 insertions, 14 deletions

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index a5d68e19b..4fb76bb82 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_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,9 +168,7 @@ 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
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index e79fc6dc9..65239a5f7 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -98,8 +98,8 @@ struct
   | DSort, DSort -> 0
   | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2
   | DCtx (tl1, tr1), DCtx (tl2, tr2)
-  | DLambda (tl1, tr1), DCtx (tl2, tr2)
-  | DApp (tl1, tr1), DCtx (tl2, tr2) ->
+  | DLambda (tl1, tr1), DLambda (tl2, tr2)
+  | DApp (tl1, tr1), DApp (tl2, tr2) ->
     let c = cmp tl1 tl2 in
     if c = 0 then cmp tr1 tr2 else c