From 5c7cd2b0c85470a96b1edb09956ebef8e5d45cfe Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 24 Nov 2002 23:13:25 +0000
Subject: Utilisation des niveaux de camlp4 pour gérer les niveaux de constr;
 améliorations diverses de l'affichage; affinement de la syntaxe et des
 options de Notation; branchement de Syntactic Definition sur Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3270 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 5be095ab8e..e3393dc6e1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,8 @@ Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
   set a notation sets has been developped for nat, Z and R
+- New command "Notation" for declaring notations simultaneously for
+  parsing and printing
 - Declarations with only implicit arguments now handled (e.g. the
   argument of nil can be set implicit; use !nil to refer to nil
   without arguments)
@@ -25,6 +27,10 @@ Library
 - Lemmas in Set from Compare_dec.v (le_lt_dec, ...) and Wf_nat.v
   (lt_wf_rec, ...) are now transparent. This may be source of
   incompatibilities.
+- Syntactic Definitions Fst, Snd, Ex, All, Ex2, AllT, ExT, ExT2,
+  ProjS1, ProjS2, Error, Value and Except are turned to
+  notations. They now must be applied (incompatibilities only in
+  unrealistic cases).
 
 Language
 
@@ -74,10 +80,13 @@ Tactics
   hypothesis was unfolded to `x < y` -> False. This is fixed. In addition,
   it can also recognize 'False' in the hypothesis and use it to solve the
   goal.
+- New syntax for Ring and Field when arguments are provided (use "Ring on" and
+  "Field on")
 
 Miscellaneous
 
 - Printing Coercion now used through the standard keywords Set/Add, Test, Print
+- "Print Term id" is an alias for "Print id"
 
 Incompatibilities
 
-- 
cgit v1.2.3