diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output-modulo-time/ltacprof_cutoff.v | 28 |
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. |