Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 26 insertions, 10 deletions

diff --git a/test-suite/output-modulo-time/ltacprof_cutoff.v b/test-suite/output-modulo-time/ltacprof_cutoff.v
index 50131470..ae5d51ba 100644
--- a/test-suite/output-modulo-time/ltacprof_cutoff.v
+++ b/test-suite/output-modulo-time/ltacprof_cutoff.v
@@ -1,12 +1,28 @@
-(* -*- 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).
+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.
+  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.