From 04b28b0c95f15fedb2e5eef26cd87b97b4e2120d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 31 Jul 2014 20:51:48 +0200
Subject: Making the error message about bullets more precise. Suggests in some
 cases the right bullet to use.

---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index ebef67e89c..50edd1795c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -166,7 +166,7 @@ Tactics
   (possible source of incompatibilities solvable by avoiding clearing
   the relevant hypotheses).
 - New construct "uconstr:c" and "type_term c" to build untyped terms.
-
+- The good bullet (-/+/*) is suggested sometimes when user gives a wrong one.
 
 Program
 
-- 
cgit v1.2.3