aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in')
-rw-r--r--test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in20
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in
new file mode 100644
index 0000000000..b49c1b1cb7
--- /dev/null
+++ b/test-suite/coq-makefile/timing/precomputed-time-tests/004-per-file-fuzz/foo.v.before-timing.in
@@ -0,0 +1,20 @@
+Chars 0 - 30 [Require~Import~Coq.Lists.List.] 0.114 secs (0.072u,0.044s)
+Chars 31 - 64 [Require~Import~Coq.ZArith.ZArith.] 0.192 secs (0.156u,0.035s)
+Chars 65 - 75 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 78 - 90 [constructor.] 0. secs (0.u,0.s)
+Chars 91 - 95 [Qed.] 0. secs (0.u,0.s)
+Chars 96 - 106 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 109 - 121 [constructor.] 0. secs (0.u,0.s)
+Chars 122 - 126 [Qed.] 0. secs (0.u,0.s)
+Chars 127 - 137 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 140 - 152 [constructor.] 0. secs (0.u,0.004s)
+Chars 153 - 157 [Qed.] 0. secs (0.u,0.s)
+Chars 158 - 168 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 171 - 183 [constructor.] 0. secs (0.u,0.s)
+Chars 184 - 188 [Qed.] 0. secs (0.u,0.s)
+Chars 189 - 199 [Goal~_~True.] 0. secs (0.u,0.s)
+Chars 202 - 214 [constructor.] 0. secs (0.u,0.s)
+Chars 215 - 219 [Qed.] 0. secs (0.u,0.s)
+Chars 220 - 277 [Goal~_~List.repeat~Z.div_eucl~...] 0. secs (0.u,0.s)
+Chars 280 - 304 [(vm_compute;~reflexivity).] 0.566 secs (0.528u,0.039s)
+Chars 305 - 309 [Qed.] 0.411 secs (0.4u,0.008s)