From e7b7dde4455a12d2b87a4052b759954f9f9243cd Mon Sep 17 00:00:00 2001 From: soubiran Date: Tue, 15 Dec 2009 14:01:56 +0000 Subject: Description of the new features of the module system (first part). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12587 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'CHANGES') diff --git a/CHANGES b/CHANGES index be86cd7ba6..9867a7e21a 100644 --- a/CHANGES +++ b/CHANGES @@ -87,6 +87,9 @@ Vernacular commands congruence schemes available to user (governed by options "Unset Case Analysis Schemes" and "Unset Congruence Schemes"). - Fixpoint/CoFixpoint now support building part or all of bodies using tactics. +- New commands for modules and module types "Include Self " and + "Include Type Self ". + Tools @@ -134,6 +137,14 @@ Library - heapsort from Heap.v of worst-case complexity O(n*n) is deprecated; - new file Sorted.v for some definitions of being sorted. +Language + +- New implementation of the module system. The sharing between non-logical + object and the management of the name-space has been improved by the new + \Delta-equivalence on qualified name. The include operator has been extended + to high-order structures (cf. libraries Numbers ans Structures to see examples). + Interactive proofs are now authorized in module type. + Changes from V8.1 to V8.2 ========================= -- cgit v1.2.3