- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"

  n'étaient pas gérés, merci à Julien). 
- Correction pb blocage CoqIDE quand le browser n'est pas déja lancé
  (utilisation pour cela de Sys.command au lieu de Unix.open_process_full).
- MAJ CHANGES et COMPATIBILITY.


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

1 files changed, 3 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index b4d8397e97..c51cbd9dcd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -93,6 +93,8 @@ Libraries (DOC TO CHECK)
 - Slight restructuration of the Logic library regarding choice and classical
   logic. Addition of files providing intuitionistic axiomatizations of
   descriptions: Epsilon.v, Description.v and IndefiniteDescription.v.
+- Definition of pred and minus made compatible with the structural
+  decreasing criterion for use in fixpoints.
 
 Notations, coercions, implicit arguments and type inference
 
@@ -497,7 +499,7 @@ Modules
   "Module Type M(Export/Import X Y: T)"
   (only for interactive definitions)
 - Construct "with" generalized to module paths:
-   T with (Definition|Module) M1.M2....Mn.l := l' (doc TODO).
+   T with (Definition|Module) M1.M2....Mn.l := l'.
 
 Notations