From a8b99e40e954ff7c1ff4858b44ffa362c225928b Mon Sep 17 00:00:00 2001 From: notin Date: Tue, 3 Jun 2008 06:41:48 +0000 Subject: Temporarily disabling automatic test for bug 1338.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11041 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/bugs/opened/shouldnotfail/1338.v | 12 ------------ test-suite/bugs/opened/shouldnotfail/1338.v-disabled | 12 ++++++++++++ 2 files changed, 12 insertions(+), 12 deletions(-) delete mode 100644 test-suite/bugs/opened/shouldnotfail/1338.v create mode 100644 test-suite/bugs/opened/shouldnotfail/1338.v-disabled diff --git a/test-suite/bugs/opened/shouldnotfail/1338.v b/test-suite/bugs/opened/shouldnotfail/1338.v deleted file mode 100644 index f383d53440..0000000000 --- a/test-suite/bugs/opened/shouldnotfail/1338.v +++ /dev/null @@ -1,12 +0,0 @@ -Require Import Omega. - -Goal forall x, 0 <= x -> x <= 20 -> -x <> 0 - -> x <> 1 -> x <> 2 -> x <> 3 -> x <>4 -> x <> 5 -> x <> 6 -> x <> 7 -> x <> 8 --> x <> 9 -> x <> 10 - -> x <> 11 -> x <> 12 -> x <> 13 -> x <> 14 -> x <> 15 -> x <> 16 -> x <> 17 --> x <> 18 -> x <> 19 -> x <> 20 -> False. -Proof. - intros. - omega. -Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1338.v-disabled b/test-suite/bugs/opened/shouldnotfail/1338.v-disabled new file mode 100644 index 0000000000..f383d53440 --- /dev/null +++ b/test-suite/bugs/opened/shouldnotfail/1338.v-disabled @@ -0,0 +1,12 @@ +Require Import Omega. + +Goal forall x, 0 <= x -> x <= 20 -> +x <> 0 + -> x <> 1 -> x <> 2 -> x <> 3 -> x <>4 -> x <> 5 -> x <> 6 -> x <> 7 -> x <> 8 +-> x <> 9 -> x <> 10 + -> x <> 11 -> x <> 12 -> x <> 13 -> x <> 14 -> x <> 15 -> x <> 16 -> x <> 17 +-> x <> 18 -> x <> 19 -> x <> 20 -> False. +Proof. + intros. + omega. +Qed. -- cgit v1.2.3