diff options
Diffstat (limited to 'test-suite/output-modulo-time')
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof.v | 2 | ||||
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_cutoff.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/output-modulo-time/ltacprof.v b/test-suite/output-modulo-time/ltacprof.v index 6611db70e..1e9e91979 100644 --- a/test-suite/output-modulo-time/ltacprof.v +++ b/test-suite/output-modulo-time/ltacprof.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs" "-profile-ltac-cutoff" "0.0") -*- *) +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) Ltac sleep' := do 100 (do 100 (do 100 idtac)). Ltac sleep := sleep'. diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v index 50131470e..3dad6271a 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: ("-emacs" "-profile-ltac") -*- *) +(* -*- coq-prog-args: ("-profile-ltac") -*- *) Require Coq.ZArith.BinInt. Ltac sleep := do 50 (idtac; let sleep := (eval vm_compute in Coq.ZArith.BinInt.Z.div_eucl) in idtac). |