- Cleanup parsing of binders, reducing to a single production for all

  binders.
- Change syntax of type class instances to better match the usual syntax of
  lemmas/definitions with name first, then arguments ":" instance.
  Update theories/Classes accordingly.
- Correct globalization of tactic references when doing Ltac :=/::=, update
  documentation.
- Remove the not so useful "(x &)" and "{{x}}" syntaxes from
  Program.Utils, and subset_scope as well.


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

1 files changed, 0 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 0fd8c3ac68..a349979fc4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -129,7 +129,6 @@ Tactic Language
   ltac function into names that do not clash with the lemmas
   parameter names used in the tactic).
 - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression.
-  (DOC TODO?)
 - "let rec ... in ... " now supported for expressions without explicit
   parameters; interpretation is lazy to the contrary of "let ... in ...";
   hence, the "rec" keyword can be used to turn the argument of a