aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2019-03-05 10:15:50 +0100
committerThéo Zimmermann2019-03-05 10:19:37 +0100
commit6188c34dd35b9d0f3a8fef6ec2c87a93614cfad8 (patch)
treeaabbc381a95c704ceb8fc2e70f1a4fdff2dbf25e
parent5f0caf7fda4fb2efec4c7e9c03b0ec155baef9ca (diff)
Remove regularly failing test from test-suite.
-rw-r--r--test-suite/output-modulo-time/ltacprof_cutoff.v28
1 files changed, 0 insertions, 28 deletions
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
deleted file mode 100644
index b7c98aa134..0000000000
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ /dev/null
@@ -1,28 +0,0 @@
-(* -*- coq-prog-args: ("-async-proofs" "off" "-profile-ltac") -*- *)
-Require Coq.ZArith.BinInt.
-Module WithIdTac.
- Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac).
-
- Ltac foo0 := idtac; sleep.
- Ltac foo1 := sleep; foo0.
- Ltac foo2 := sleep; foo1.
- Goal True.
- foo2.
- Show Ltac Profile CutOff 47.
- constructor.
- Qed.
-End WithIdTac.
-
-Module TestEval.
- Ltac sleep := let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac.
-
- Ltac foo0 := idtac; do 50 (idtac; sleep).
- Ltac foo1 := sleep; foo0.
- Ltac foo2 := sleep; foo1.
- Goal True.
- Reset Ltac Profile.
- foo2.
- Show Ltac Profile CutOff 47.
- constructor.
- Qed.
-End TestEval.