Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.

The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.

Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.

2 files changed, 37 insertions, 2 deletions

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ee7b94b0d..20a7448dc 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -166,6 +166,10 @@ and e_my_find_search db_list local_db hdc concl =
   in
   let tac_of_hint =
     fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
+      let b = match Hints.repr_hint t with
+      | Unfold_nth _ -> 1
+      | _ -> b
+      in
       (b,
         let tac = function
         | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
@@ -245,8 +249,8 @@ module SearchProblem = struct
     let d = s'.depth - s.depth in
     let d' = Int.compare s.priority s'.priority in
     let nbgoals s = List.length (sig_it s.tacres) in
-    if not (Int.equal d' 0) then d'
-    else if not (Int.equal d 0) then d
+    if not (Int.equal d 0) then d
+    else if not (Int.equal d' 0) then d'
     else Int.compare (nbgoals s) (nbgoals s')
 
   let branching s =
diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v
new file mode 100644
index 000000000..bf0e570ab
--- /dev/null
+++ b/test-suite/bugs/closed/4429.v
@@ -0,0 +1,31 @@
+Require Import Arith.Compare_dec.
+Require Import Unicode.Utf8.
+
+Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
+  match n with
+    | O    => x
+    | S n' => f (my_nat_iter n' f x)
+  end.
+
+Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
+  match mn with
+    | (0, 0)       => 0
+    | (0, S n')    => S n'
+    | (S m', 0)    => S m'
+    | (S m', S n') =>
+      match le_gt_dec (S m') (S n') with
+        | left  _ => f (S m', S n' - S m')
+        | right _ => f (S m' - S n', S n')
+      end
+  end.
+
+Axiom max_correct_l : ∀ m n : nat, m <= max m n.
+Axiom max_correct_r : ∀ m n : nat, n <= max m n.
+
+Hint Resolve max_correct_l max_correct_r : arith.
+
+Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
+Proof.
+  intros.
+  Timeout 3 eauto with arith.
+Qed.