7 files changed, 9 insertions, 7 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/opened/shouldnotfail/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v
index abf854553..abf854553 100644
--- a/test-suite/bugs/opened/shouldnotfail/1776.v
+++ b/test-suite/bugs/closed/shouldsucceed/1776.v
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.
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index a24ad124e..f23198b0f 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,7 +2,7 @@
      : Z
 fun f : nat -> Z => (f 0%nat + 0)%Z
      : (nat -> Z) -> Z
-fun x : positive => Zpos x~0)
+fun x : positive => Zpos x~0
      : positive -> Z
 fun x : positive => (Zpos x + 1)%Z
      : positive -> Z
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 6a5bf58b6..74d87ffa7 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -322,7 +322,7 @@ Extraction test24.
 Require Import Gt.
 Definition loop (Ax:Acc gt 0) :=
   (fix F (a:nat) (b:Acc gt a) {struct b} : nat :=
-     F (S a) (Acc_inv b (gt_Sn_n a))) 0 Ax.
+     F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax.
 Extraction loop.
 (* let loop _ =
   let rec f a =