From 574e510ba069f1747ecb1e5a17cf86c902d79d44 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Nov 2015 18:40:32 +0100
Subject: 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.
---
 tactics/eauto.ml4             |  8 ++++++--
 test-suite/bugs/closed/4429.v | 31 +++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/4429.v

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ee7b94b0d1..20a7448dcb 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 0000000000..bf0e570ab8
--- /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.
-- 
cgit v1.2.3