Merge from Lionel Elie Mamane's private branch:

 - 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

1 files changed, 7 insertions, 0 deletions

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
+<lionel@mamane.lu> 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)