From d67f446540543024c8afceff65c2356055ecd2bf Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 24 Jan 2008 13:21:32 +0000
Subject: Fermeture du bug #1754

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10472 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/1754.v | 24 ++++++++++++++++++++++++
 test-suite/bugs/opened/shouldnotfail/1754.v | 24 ------------------------
 2 files changed, 24 insertions(+), 24 deletions(-)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/1754.v
 delete mode 100644 test-suite/bugs/opened/shouldnotfail/1754.v

diff --git a/test-suite/bugs/closed/shouldsucceed/1754.v b/test-suite/bugs/closed/shouldsucceed/1754.v
new file mode 100644
index 0000000000..06b8dce851
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1754.v
@@ -0,0 +1,24 @@
+Axiom hp : Set.
+Axiom cont : nat -> hp -> Prop.
+Axiom sconj : (hp -> Prop) -> (hp -> Prop) -> hp -> Prop.
+Axiom sconjImpl : forall h A B,
+  (sconj A B) h -> forall (A' B': hp -> Prop),
+    (forall h', A h' -> A' h') ->
+    (forall h', B h' -> B' h') ->
+    (sconj A' B') h.
+
+Definition cont' (h:hp) := exists y, cont y h.
+
+Lemma foo : forall h x y A,
+  (sconj (cont x) (sconj (cont y) A)) h ->
+  (sconj cont' (sconj cont' A)) h.
+Proof.
+  intros h x y A H.
+  eapply sconjImpl.
+  2:intros h' Hp'; econstructor; apply Hp'.
+  2:intros h' Hp'; eapply sconjImpl.
+  3:intros h'' Hp''; econstructor; apply Hp''.
+  3:intros h'' Hp''; apply Hp''.
+  2:apply Hp'.
+  clear H.
+Admitted.
diff --git a/test-suite/bugs/opened/shouldnotfail/1754.v b/test-suite/bugs/opened/shouldnotfail/1754.v
deleted file mode 100644
index 06b8dce851..0000000000
--- a/test-suite/bugs/opened/shouldnotfail/1754.v
+++ /dev/null
@@ -1,24 +0,0 @@
-Axiom hp : Set.
-Axiom cont : nat -> hp -> Prop.
-Axiom sconj : (hp -> Prop) -> (hp -> Prop) -> hp -> Prop.
-Axiom sconjImpl : forall h A B,
-  (sconj A B) h -> forall (A' B': hp -> Prop),
-    (forall h', A h' -> A' h') ->
-    (forall h', B h' -> B' h') ->
-    (sconj A' B') h.
-
-Definition cont' (h:hp) := exists y, cont y h.
-
-Lemma foo : forall h x y A,
-  (sconj (cont x) (sconj (cont y) A)) h ->
-  (sconj cont' (sconj cont' A)) h.
-Proof.
-  intros h x y A H.
-  eapply sconjImpl.
-  2:intros h' Hp'; econstructor; apply Hp'.
-  2:intros h' Hp'; eapply sconjImpl.
-  3:intros h'' Hp''; econstructor; apply Hp''.
-  3:intros h'' Hp''; apply Hp''.
-  2:apply Hp'.
-  clear H.
-Admitted.
-- 
cgit v1.2.3