Ajout d'une syntaxe pour Reals.

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

1 files changed, 7 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 07417a10f..5d360e0f6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -9,8 +9,6 @@ Parsing
 - "command" in grammars and quotations is now "constr" as in
   pretty-printing rules
 
-
-
 Syntaxe des constructions
 
 - Consecutive as in patterns are forbidden
@@ -26,6 +24,13 @@ Syntaxe des constructions
   cas de clauses par défaut redondantes auquel cas la première est prise
   avec un avertissement.
 
+Syntaxe des theories
+
+- Ajout d'une syntaxe pour les reels: ``Rexpr``.
+  Point noir du aux constantes: 
+     (Rplus (Rplus (Rplus R1 R1) (Rplus R1 R1)) R1) est toujours (2+2+1) 
+               au lieu de 2+2+1 
+
 Vernac
 
 - Ajout de la syntaxe "[" phrase_1 ... phrase_n"]." pour grouper des