Adding a "time" tactical for benchmarking purposes. In case the tactic

backtracks, print time spent in each of successive calls.

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 0fa460dca2..6494173b58 100644
--- a/CHANGES
+++ b/CHANGES
@@ -119,6 +119,7 @@ Tactics
   error messages.
 - Tactic "subst id" now supports id occurring in dependent local definitions.
 - Bugs fixed about intro-pattern "*" might lead to some rare incompatibilities.
+- New tactical "time" to display time spent executing its argument.
 
 Program