From c71aa6bd368b801bb17d4da69d1ab1e2bd7cbf39 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 7 Nov 2015 07:20:34 +0100
Subject: Fixing logical bugs in the presence of let-ins in computiong
 primitive projections.

- lift accounting for the record missing in computing the subst from
  fields to projections of the record
- substitution for parameters should not lift the local definitions
- typo in building the latter (subst -> letsubst)
---
 test-suite/success/primitiveproj.v | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 125615c535..281d707cb3 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -194,4 +194,17 @@ Record wrap (A : Type) := { unwrap : A; unwrap2 : A }.
 Definition term (x : wrap nat) := x.(unwrap).
 Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x.
 Recursive Extraction term term'.
-(*Unset Printing Primitive Projection Parameters.*)
\ No newline at end of file
+(*Unset Printing Primitive Projection Parameters.*)
+
+(* Primitive projections in the presence of let-ins (was not failing in beta3)*)
+
+Set Primitive Projections.
+Record s (x:nat) (y:=S x) := {c:=x; d:x=c}.
+Lemma f : 0=1.
+Proof.
+Fail apply d.
+(*
+split.
+reflexivity.
+Qed.
+*)
-- 
cgit v1.2.3


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.
---
 test-suite/bugs/closed/4429.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 test-suite/bugs/closed/4429.v

(limited to 'test-suite')

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