Merge PR #6381: A version of [time] that works on constr evaluation

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 24f358078..c155bb52f 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