diff options
| -rw-r--r-- | tactics/eauto.ml4 | 8 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4429.v | 31 |
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. |