From 57eec1e1e4efd09f5181297d87b1908c284e6951 Mon Sep 17 00:00:00 2001
From: notin
Date: Wed, 26 Mar 2008 17:22:36 +0000
Subject: 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
---
 test-suite/bugs/closed/shouldsucceed/1322.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1414.v |  2 +-
 test-suite/bugs/closed/shouldsucceed/1448.v |  2 ++
 test-suite/bugs/closed/shouldsucceed/1776.v | 22 ++++++++++++++++++++++
 test-suite/bugs/closed/shouldsucceed/846.v  |  6 +++---
 test-suite/bugs/opened/shouldnotfail/1776.v | 22 ----------------------
 test-suite/output/ZSyntax.out               |  2 +-
 test-suite/success/extraction.v             |  2 +-
 8 files changed, 31 insertions(+), 29 deletions(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1776.v
 delete mode 100644 test-suite/bugs/opened/shouldnotfail/1776.v

diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v
index 01c06f2c40..7e21aa7ce3 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 9c2686ceb6..d3c008087b 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 bd016c9953..fe3b4c8b41 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 0000000000..abf854553b
--- /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 95bbab92a3..a963b225fe 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/bugs/opened/shouldnotfail/1776.v b/test-suite/bugs/opened/shouldnotfail/1776.v
deleted file mode 100644
index abf854553b..0000000000
--- a/test-suite/bugs/opened/shouldnotfail/1776.v
+++ /dev/null
@@ -1,22 +0,0 @@
-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/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index a24ad124eb..f23198b0f3 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 6a5bf58b64..74d87ffa7e 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 =
-- 
cgit v1.2.3