aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES2
1 files changed, 1 insertions, 1 deletions
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