Added support for definition of fixpoints using tactics.

Fixed some bugs in -beautify and robustness of {struct} clause.

Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.



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

1 files changed, 4 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index b6744e25d3..627408cc88 100644
--- a/CHANGES
+++ b/CHANGES
@@ -42,6 +42,9 @@ Tactics
 - A new tactic name "exfalso" for the use of 'ex-falso quodlibet' principle.
   This tactic is simply a shortcut for "elimtype False".
 - Added support for Leibniz-rewriting of dependent hypotheses.
+- Binders given before ":" in lemmas are now automatically
+  introduced in the context (possible source of incompatibility that can be
+  avoided by unsetting option "Automatic Introduction").
 
 Tactic Language
 
@@ -75,6 +78,7 @@ Vernacular commands
 - Made support for automatic generation of case analysis schemes and
   congruence schemes available to user (governed by options "Unset
   Case Analysis Schemes" and "Unset Congruence Schemes").
+- Fixpoint/CoFixpoint now support building part or all of bodies using tactics.
 
 Tools