Revise syntax of Hint Cut

As noticed by C. Cohen it was confusingly different from standard
notation.

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