diff options
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_cutoff.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index ae5d51bae8..b7c98aa134 100644 --- a/test-suite/output-modulo-time/ltacprof_cutoff.v +++ b/test-suite/output-modulo-time/ltacprof_cutoff.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-profile-ltac") -*- *) +(* -*- 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). |