From 35a8ced36108db7ce46eab47c6cd0d6b8028b20c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 8 Oct 2003 12:42:07 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index c62a6c243d..5bbb723dba 100644
--- a/CHANGES
+++ b/CHANGES
@@ -46,6 +46,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
+
+Commands
+
+- new coqtop/coqc option -dont-load-proofs not to load opaque proofs in memory
 
 Gallina
 
@@ -100,6 +106,7 @@ Tactics
 - A NewInduction naming bug for inductive types with functional
   arguments (e.g. the accessibility predicate) has been fixed (source
   of incompatibilities)
+- Symmetry now applies to hypotheses too
 
 Bugs
 
-- 
cgit v1.2.3