diff options
author | Jason Gross <jgross@mit.edu> | 2017-12-12 12:00:25 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-12-14 18:02:41 -0500 |
commit | 29644bf0814945cbf2b4388b8f8bd19f109503a0 (patch) | |
tree | ca37a531989f7c329d78dda769f1f54dc7617ea3 /test-suite/output-modulo-time/ltacprof_abstract.v | |
parent | b270ad686075e5579dc3826fafdc324ea339785c (diff) |
Make [abstract] nodes show up in the Ltac profile
This closes #5082 and closes #5778, but makes #6404 apply to `abstract`
as well as `transparent_abstract`. This is unfortunate, but I think it
is worth it to get `abstract` in the profile (and therefore not
misassign the time spent sending the subproof to the kernel). Another
alternative would have been to add a dedicated entry to `ltac_call_kind`
for `TacAbstract`, but I think it's better to just deal with #6404 all
at once.
The "better" solution here would have been to move `abstract` out of the
Ltac syntax tree and define it via `TACTIC EXTEND` like
`transparent_abstract`. However, the STM relies on its ability to
recognize `abstract` and `solve [ abstract ... ]` syntactically so that
it can handle `par: abstract`.
Note that had to add locations to `TacAbstract` nodes, as I could not
figure out how to call `push_trace` otherwise.
Diffstat (limited to 'test-suite/output-modulo-time/ltacprof_abstract.v')
-rw-r--r-- | test-suite/output-modulo-time/ltacprof_abstract.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output-modulo-time/ltacprof_abstract.v b/test-suite/output-modulo-time/ltacprof_abstract.v new file mode 100644 index 000000000..10a76309e --- /dev/null +++ b/test-suite/output-modulo-time/ltacprof_abstract.v @@ -0,0 +1,8 @@ +(* -*- coq-prog-args: ("-profile-ltac-cutoff" "0.0") -*- *) +Ltac sleep' := do 100 (do 100 (do 100 idtac)). +Ltac sleep := sleep'. + +Theorem x : True. +Proof. + idtac. idtac. abstract (sleep; constructor). +Defined. |