- Cleaning (unification of ML names, removal of obsolete code,

  reorganization of code) and documentation (in pcoq.mli) of the code
  for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
  Notation, Notation); merged the two copies of interp_entry_name to
  avoid they diverge.  
- Added support in Tactic Notation for ne_..._list_sep in general and
  for (ne_)ident_list(_sep) in particular.



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

1 files changed, 4 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index eb4245bd1d..2ef2ab93b8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,10 @@ Tactics
 - Tactic "tauto" now proves classical tautologies as soon as classical logic
   (i.e. library Classical_Prop or Classical) is loaded.
 
+Tactic Language
+
+- Support for parsing non-empty lists with separators in tactic notations.
+
 Vernacular commands
 
 - New command "Timeout <n> <command>." interprets a command and a timeout