Merge PR #745: Add timing scripts

1 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 4e95f9d4c8..91abaa10b1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -95,6 +95,11 @@ Tools
   The current version contains code for retro compatibility that prints
   warnings when a deprecated feature is used.  Please upgrade your _CoqProject
   accordingly.
+  * Additionally, coq_makefile-made Makefiles now support experimental timing
+    targets `pretty-timed`, `pretty-timed-before`, `pretty-timed-after`,
+    `print-pretty-timed-diff`, `print-pretty-single-time-diff`,
+    `all.timing.diff`, and the variable `TIMING=1` (or `TIMING=before` or
+    `TIMING=after`); see the documentation for more details.
 
 Build Infrastructure