- Nouvelle option "Set Printing Existential Instances" pour forcer

  l'affichage des instances des evars.
- Nouveaux boutons "interrupteurs" pour activer/désactiver à volonté
  l'affichage des implicites, coercions, notations, etc dans CoqIDE
  (reste à trouver des icônes appropriées !).


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

1 files changed, 4 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index f18e1c5752..477faaab41 100644
--- a/CHANGES
+++ b/CHANGES
@@ -34,7 +34,9 @@ Vernacular commands
 - Added option "Set Equality Scheme" to make automatic the declaration 
   of the boolean equality when possible.
 - Source of universe inconsistencies now printed when option 
-  "Set Printing Universes" is activated,
+  "Set Printing Universes" is activated.
+- New option "Set Printing Existential Instances" for making the display of
+  existential variable instances explicit.
 - Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the 
   "compute"/"cbv" reduction strategy, respectively meaning reduce only, or 
   everything but, the constants id1 ... idn. "lazy" alone or followed by
@@ -283,6 +285,7 @@ Tools
 - CoqIDE font defaults to monospace so as indentation to be meaningful.
 - CoqIDE supports Definition/Parameter/Inductive in middle of a proof.
 - Undoing non-tactic commands in CoqIDE works faster.
+- New CoqIDE buttons for activating display of various implicit informations.
 
 Miscellaneous