5 files changed, 29 insertions, 5 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v
index 01c06f2c4..7e21aa7ce 100644
--- a/test-suite/bugs/closed/shouldsucceed/1322.v
+++ b/test-suite/bugs/closed/shouldsucceed/1322.v
@@ -18,7 +18,7 @@ Variable F : I -> Type.
 Variable F_morphism : forall i j, I_eq i j -> F i = F j.
 
 
-Add Morphism F with signature I_eq ==> eq as F_morphism2.
+Add Morphism F with signature I_eq ==> (@eq _) as F_morphism2.
 Admitted.
 
 End transition_gen.
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 9c2686ceb..d3c008087 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -1,4 +1,4 @@
-Require Import ZArith Coq.Program.Utils.
+Require Import ZArith Coq.Program.Wf Coq.Program.Utils.
 
 Parameter data:Set.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/shouldsucceed/1448.v
index bd016c995..fe3b4c8b4 100644
--- a/test-suite/bugs/closed/shouldsucceed/1448.v
+++ b/test-suite/bugs/closed/shouldsucceed/1448.v
@@ -1,7 +1,9 @@
 Require Import Relations.
+Require Import Setoid.
 Require Import Ring_theory.
 Require Import Ring_base.
 
+
 Variable R : Type.
 Variable Rone Rzero : R.
 Variable Rplus Rmult Rminus : R -> R -> R.
diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v
new file mode 100644
index 000000000..abf854553
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1776.v
@@ -0,0 +1,22 @@
+Axiom pair : nat -> nat -> nat -> Prop.
+Axiom pl : (nat -> Prop) -> (nat -> Prop) -> (nat -> Prop).
+Axiom plImpR : forall k P Q,
+  pl P Q k -> forall (Q':nat -> Prop),
+    (forall k', Q k' -> Q' k') ->
+    pl P Q' k.
+
+Definition nexists (P:nat -> nat -> Prop) : nat -> Prop :=
+  fun k' => exists k, P k k'.
+
+Goal forall a A m,
+  True ->
+  (pl A (nexists (fun x => (nexists 
+    (fun y => pl (pair a (S x)) (pair a (S y))))))) m.
+Proof.
+  intros.
+  eapply plImpR; [ | intros; econstructor; econstructor; eauto].
+  clear H;
+    match goal with
+       | |- (pl _ (pl (pair _ ?x) _)) _ => replace x with 0
+    end.
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v
index 95bbab92a..a963b225f 100644
--- a/test-suite/bugs/closed/shouldsucceed/846.v
+++ b/test-suite/bugs/closed/shouldsucceed/846.v
@@ -138,15 +138,15 @@ Proof.
   right; assumption.
   intros l _ r.
   apply (step (A:=L' A l)).
-  exact (inl (inl r)).
+  exact (inl _ (inl _ r)).
   intros l _ r1 _ r2.
   apply (step (A:=L' A l)).
   (* unfold L' in * |- *.
   Check 0. *)
-  exact (inl (inr (pair r1 r2))).
+  exact (inl _ (inr _ (pair r1 r2))).
   intros l _ r.
   apply  (step (A:=L' A l)).
-  exact (inr r).
+  exact (inr _ r).
 Defined.
 
 Definition L'inG: forall A: Set, L' A (true::nil) -> G A.