diff options
Diffstat (limited to 'debian/patches/remove-time-sensitive-tests.patch')
| -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 @@ |