From bce104e3bb510fb10df2ecddebb47514328f2b8d Mon Sep 17 00:00:00 2001 From: lmamane Date: Wed, 10 Jan 2007 15:44:44 +0000 Subject: Merge from Lionel Elie Mamane's private branch: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Makefile: Option (environment variable NO_RECOMPILE_LIB) to not recompile the whole standard library just because the coq binaries got rebuilt. - Infrastructure to change the object pretty-printers at runtime. - Use that infrastructure to make coqtop-protocol with Pcoq trees and Pcoq-protocol with pretty-printed terms possible in coq-interface. - Make "Back(track)" into closed sections, modules and module types "Just Work™". - Modernise/generalise Pcoq protocol a bit, make some of its warts optional. - Implement "Show." in Pcoq mode. - Add Rpow_def.vo to REALSBASEVO so that its dependencies are computed (and used). - "make revision" now handles GNU Arch / tla in addition to svn. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9476 85f007b7-540e-0410-9357-904b9bb8a0f7 --- COPYRIGHT | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'COPYRIGHT') diff --git a/COPYRIGHT b/COPYRIGHT index ac7d87dfa..2cbb6fbce 100644 --- a/COPYRIGHT +++ b/COPYRIGHT @@ -5,6 +5,13 @@ University Paris Sud. Copyright 1999-2004 The Coq development team, INRIA-CNRS, University Paris Sud, All rights reserved. +This version contains modifications by Lionel Elie Mamane + done while under employment of the Radboud +University Nijmegen. However, no copyright-assignment-to-employer +agreement was signed, and copyright of articles and books written on +work time rest with the employee. By analogy, it is Lionel's opinion +that copyright on these changes rests with him. + This product includes also software developed by Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface, parsing/search.ml) -- cgit v1.2.3