MAJ

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

1 files changed, 35 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index 27c058a1de..ce4c9d5617 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,6 +16,13 @@ A revision of the standard library and of concrete syntax of Coq, including
   backquote or double-backquotes delimiters.
 - Symbolic notations for lists and argument of nil is implicit
 
+Logic
+
+- Set now predicate by default
+- New option -strongly-constructive to set Set impredicative
+- New option -strongly-classical to forbid Set to be set impredicative
+  in future development
+
 Syntax translator
 
 - Unsafe for annotation Cases when constructors coercions are used or when
@@ -46,9 +53,12 @@ Vernacular commands
 - Notation now mandatorily requires a precedence and associativity
   (default was to set precedence to 1 and associativity to none)
 - New command "About name" for light printing of type, implicit arguments, etc.
-- New declaration "Conjecture" and command "Admitted" to declare incompletely
-  proven statement as axioms
+- New command "Admitted" to declare incompletely proven statement as axioms
+- New keyword "Conjecture" to declare an axiom intended to be provable
 - New command "SearchNamed" for searching objects by components of their name
+- SearchAbout can now search for lemmas referring to more than one constant
+  and on substrings of the name of the lemma
+- Locate now searches for all names having a given suffix
 
 Commands
 
@@ -80,10 +90,13 @@ Grammar extensions
 
 Library
 
-- "true_sub" used in Zplus now a definition, not a local one
+- New library NArith on binary natural numbers
+- "true_sub" used in Zplus now a definition, not a local one (source
+  of incompatibilities in proof referring to true_sub, may need extra Unfold)
 - Some lemmas about minus moved from fast_integer to Arith/Minus.v
-  (le_minus, lt_mult_left)
-- Lemma add_x_x moved from auxiliary.v to fast_integer.v
+  (le_minus, lt_mult_left) (theoretical source of incompatibilities)
+- Several lemmas moved from auxiliary.v and zarith_aux.v to
+  fast_integer.v (theoretical source of incompatibilities)
 - New file about the factorial function in Arith
 - Variables names of iff_trans changed (source of incompatibilities)
 
@@ -109,6 +122,12 @@ Tactics
   of incompatibilities)
 - Symmetry now applies to hypotheses too
 - Inversion now accept a "as [ ... ]" option to name the hypotheses
+- Contradiction now looks also for contradictory hypotheses stating ~A and A
+  (source of incompatibility)
+- "Contradiction c" try to find an hypothesis in context which
+  contradicts the type of c
+- Ring applies to new library NArith (require file NArithRing)
+- Field now works on types in Set
 
 Bugs
 
@@ -120,6 +139,17 @@ Miscellaneous
 - Implicit parameters of inductive types definition now taken into
   account for infering other implicit arguments
 
+Incompatibilities
+
+- Persistence of true_sub (4 incompatibilities in Coq user contributions)
+- Restructuration in ZArith and Arith (no incompatibility in Coq user contribs)
+- Variable names of some constants changed for a better uniformity (2 changes
+  in Coq user contributions)
+- Naming of quantified names in goal now avoid global names (2 occurrences)
+- NewInduction naming for inductive types with functional arguments
+   (no incompatibility)
+- Contradiction now solve more goals (source of 1 incompatibility)
+
 Changes from V7.3.1 to V7.4
 ===========================