diff options
| author | Maxime Dénès | 2018-12-21 15:11:17 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-09 11:18:31 +0100 |
| commit | 62ece342f56380e54ecfe2b403159e9b115a8406 (patch) | |
| tree | 1bc623dc0cf90dd9fef89c005f4881719d5ed17e | |
| parent | 48ae6cec009554a337f64b0402daea2c653e25e2 (diff) | |
Test ltacprof in sequential mode
Scripting these commands in async mode does not really make sense.
| -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). |