From 2194292dbe88674fd9a606bb22f28d332f670f77 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jun 2016 23:24:57 +0200
Subject: Revise syntax of Hint Cut

As noticed by C. Cohen it was confusingly different from standard
notation.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

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
-- 
cgit v1.2.3