aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-12-14 14:12:47 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-12-14 14:12:47 -0500
commit4024286d9fdd13e5ec4c474b1dae4ce58ac41683 (patch)
treeb1e9a9c49b178782b4f6c9f903173e9d58734a11 /CHANGES
parent90d79c5656c394909ffc9343b903dd1231abd7a4 (diff)
Add documentation for time_constr
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
1 files changed, 2 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index 9ac3c3c32..e46fc2eba 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,6 +35,8 @@ Tactics
- Tactic "decide equality" now able to manage constructors which
contain proofs.
- Added tactics reset ltac profile, show ltac profile (and variants)
+- Added tactics restart_timer, finish_timing, and time_constr as an
+ experimental way of timing Ltac's evaluation phase
Vernacular Commands