Diverses petites modifs dans la test-suite:

  test-suite/output/ZSyntax.out
    typo

  test-suite/bugs/closed/shouldsucceed/1776.v
    bug closed

  test-suite/success/extraction.v
  test-suite/success/extraction.v
  test-suite/bugs/closed/shouldsucceed/846.v
    backtrack sur le commit 10639

  test-suite/bugs/closed/shouldsucceed/1322.v:
    petites modifications suite aux changement de setoid_replace

  test-suite/bugs/closed/shouldsucceed/1414.v:
    petites modifications suite aux changement dans Program




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 7 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/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.