diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 13:41:53 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 15:09:56 -0500 |
| commit | 7cbefd56ba087ae51bc618db5bc72a51d10dedbf (patch) | |
| tree | 9e9a7a703c910b6cd90c2dbdb981f383d5f3a577 | |
| parent | 4e783ae1e73875e34026baff95afc46351746098 (diff) | |
Disable test 4366, which is too time-sensitive for MIPS
| -rw-r--r-- | debian/patches/remove-time-sensitive-tests.patch | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/debian/patches/remove-time-sensitive-tests.patch b/debian/patches/remove-time-sensitive-tests.patch index 8a5d640b..8a0052db 100644 --- a/debian/patches/remove-time-sensitive-tests.patch +++ b/debian/patches/remove-time-sensitive-tests.patch @@ -30,6 +30,24 @@ too slowly to pass on platforms without OCaml native compilers (MIPS). - let x := constr:(let n := 17 in do_n n = do_n n) in - let y := (eval lazy in x) in - assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *) +--- a/test-suite/bugs/closed/4366.v ++++ /dev/null +@@ -1,15 +0,0 @@ +-Fixpoint stupid (n : nat) : unit := +-match n with +-| 0 => tt +-| S n => +- let () := stupid n in +- let () := stupid n in +- tt +-end. +- +-Goal True. +-Proof. +-pose (v := stupid 24). +-Timeout 4 vm_compute in v. +-exact I. +-Qed. --- a/test-suite/bugs/closed/4429.v +++ /dev/null @@ -1,31 +0,0 @@ |