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/opened/shouldnotfail/1776.v | 22 ----------------------
 1 file changed, 22 deletions(-)
 delete mode 100644 test-suite/bugs/opened/shouldnotfail/1776.v

(limited to 'test-suite/bugs/opened')

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.
-- 
cgit v1.2.3