aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES b/CHANGES
index db27f82001..5e71343d7a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,6 +29,10 @@ Tactics
instead (potential source of incompatibilities).
- New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO).
+Hints
+
+- Revised the syntax of [Hint Cut] to follow standard notation for regexps.
+
Program
- The "Shrink Obligations" flag now applies to all obligations, not only those