2 files changed, 45 insertions, 1 deletions
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.
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.
+*)