1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Description: longer timeout to avoid failure on riscv64 architecture
Author: Ralf Jung
Forwarded: https://gitlab.mpi-sws.org/iris/iris/-/issues/571
--- coq-iris.orig/tests/proofmode.v
+++ coq-iris/tests/proofmode.v
@@ -733,7 +733,7 @@
performs acceptably when the number of quantifiers becomes larger. A naive
implementation of this functionality would face an exponential slowdown. *)
iIntros "[HP HΦ]".
- Timeout 1 iFrame "HP".
+ Timeout 2 iFrame "HP".
Timeout 1 iFrame "HΦ".
repeat (iExists 0; iSplit); eauto.
Qed.
|
