From 8987bf66fe39896ce3a4cdb2acc9146f64fd9e8b Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 12 Dec 2011 17:13:20 +0000 Subject: CHANGES: some more updates git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14791 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/CHANGES b/CHANGES index 669c1d0e0..fa7e19aa9 100644 --- a/CHANGES +++ b/CHANGES @@ -101,6 +101,7 @@ Module System The level of a parameter can be fixed by "Parameter Inline(30) foo". When levels aren't given, the default value is 100. One can also use the flag "Set Inline Level ..." to set a level. TODO: DOC! +- Print Assumptions should now handle correctly opaque modules (#2168) - Print Module (Type) now tries to print more details, such as types and bodies of the module elements. Note that Print Module Type could be used on a module to display only its interface. The option @@ -166,6 +167,7 @@ Internal infrastructure - Opaque proofs are now loaded lazily by default. This allows to be almost as fast as -dont-load-proofs, while being safer (no creation of axioms) and avoiding feature restrictions (Print and Print Assumptions work ok). +- Revised hash-consing code allowing more sharing of memory - Experimental support added for camlp4 (the one provided alongside ocaml), simply pass option -usecamlp4 to ./configure. By default camlp5 is used. - Revised build system: no more stages in Makefile thanks to some recursive @@ -191,6 +193,7 @@ Extraction extraction to optimize singleton container types. DOC TODO - The extraction now identifies and properly rejects a particular case of universe polymorphism it cannot handle yet (the pair (I,I) being Prop). +- Support of anonymous fields in record (#2555). CoqIDE @@ -199,6 +202,10 @@ CoqIDE (cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts, the Windows version of coqide now requires Windows >= XP SP1. +- The communication between CoqIDE and Coqtop is now done via a dialect + of XML (DOC TODO). +- The backtrack engine of CoqIDE has been reworked, it now used the + "Backtrack" command similarly to ProofGeneral. - The Coqide parsing of sentences has be reworked and now supports tactic delimitation via { }. - Coqide now accepts the Abort command (wish #2357). -- cgit v1.2.3