- Addition of "Hint Resolve ->" and "Hint Resolve <-" continued: it

  revealed a too strict test for detection of inferable metas in
  Clenv. Restored tolerance for unbound names in interactive tactic use.
- Moral removals of some captures of Not_found in Environ.evaluable_* since
  kernel is assumed to deal with existing names.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12122 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 2ef2ab93b..2fae9a7e7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,6 +17,8 @@ Tactics
 - Tactic "idtac" now displays its list arguments.
 - Tactic "tauto" now proves classical tautologies as soon as classical logic
   (i.e. library Classical_Prop or Classical) is loaded.
+- New "Hint Resolve ->" (or "<-") for declaring iff's as oriented
+  hints (wish #2104).
 
 Tactic Language