4 files changed, 41 insertions, 31 deletions
diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v
index 0b576db6b3..820022d995 100644
--- a/test-suite/bugs/opened/1596.v
+++ b/test-suite/bugs/opened/1596.v
@@ -2,7 +2,6 @@ Require Import Relations.
 Require Import FSets.
 Require Import Arith.
 Require Import Omega.
-Unset Standard Proposition Elimination Names.
 
 Set Keyed Unification.
 
diff --git a/test-suite/bugs/opened/3424.v b/test-suite/bugs/opened/3424.v
new file mode 100644
index 0000000000..d1c5bb68f9
--- /dev/null
+++ b/test-suite/bugs/opened/3424.v
@@ -0,0 +1,24 @@
+Set Universe Polymorphism.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
+Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }.
+Inductive trunc_index : Type := minus_two | trunc_S (x : trunc_index).
+Bind Scope trunc_scope with trunc_index.
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+Notation minus_one:=(trunc_S minus_two).
+Notation "0" := (trunc_S minus_one) : trunc_scope.
+Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
+Notation IsHProp := (IsTrunc minus_one).
+Notation IsHSet := (IsTrunc 0).
+Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }.
+Proof.
+intros.
+eexists.
+(* exact (H' a b). *)
+(* Undo. *)
+Fail apply (H' a b).
+exact (H' a b).
+Qed.
diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v
deleted file mode 100644
index cfad763572..0000000000
--- a/test-suite/bugs/opened/3926.v
+++ /dev/null
@@ -1,30 +0,0 @@
-Notation compose := (fun g f x => g (f x)).
-Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope.
-Open Scope function_scope.
-Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope.
-Arguments idpath {A a} , [A] a.
-Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end.
-Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }.
-Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope.
-Local Open Scope equiv_scope.
-Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x.
-Generalizable Variables A B C f g.
-Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000
-  := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1).
-Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g
-  := Build_IsEquiv _ _ g (f ^-1).
-Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000
-  := Build_IsEquiv B A f^-1 f.
-Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C}
-  `{IsEquiv A B f} `{IsEquiv A C (g o f)}
-  : IsEquiv g.
-Proof.
-  Unset Typeclasses Modulo Eta.
-  exact (isequiv_homotopic (compose (compose g f) f^-1)
-                           (fun b => ap g (eisretr f b))) || fail "too early".
-  Undo.
-  Set Typeclasses Modulo Eta.
-  Set Typeclasses Dependency Order.
-  Set Typeclasses Debug.
-  Fail exact (isequiv_homotopic (compose (compose g f) f^-1)
-                           (fun b => ap g (eisretr f b))).
diff --git a/test-suite/bugs/opened/6602.v b/test-suite/bugs/opened/6602.v
new file mode 100644
index 0000000000..3690adf90a
--- /dev/null
+++ b/test-suite/bugs/opened/6602.v
@@ -0,0 +1,17 @@
+Require Import Omega.
+
+Lemma test_nat:
+  forall n, (5 + pred n <= 5 + n).
+Proof.
+  intros.
+  zify.
+  omega.
+Qed.
+
+Lemma test_N:
+  forall n, (5 + N.pred n <= 5 + n)%N.
+Proof.
+  intros.
+  zify.
+  omega.
+Qed.