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: - 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 --- contrib/interface/COPYRIGHT | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'contrib/interface/COPYRIGHT') diff --git a/contrib/interface/COPYRIGHT b/contrib/interface/COPYRIGHT index 2fb11c6bcf..ff567a5466 100644 --- a/contrib/interface/COPYRIGHT +++ b/contrib/interface/COPYRIGHT @@ -3,6 +3,7 @@ (* Coq support for the Pcoq Graphical Interface of Coq *) (* *) (* Copyright (C) 1999-2004 INRIA Sophia-Antipolis (Lemme team) *) +(* Copyright (C) 2006 Lionel Elie Mamane *) (* *) (*****************************************************************************) @@ -10,6 +11,9 @@ The current directory contrib/interface implements Coq support for the Pcoq Graphical Interface of Coq. It has been developed by Yves Bertot with contributions from Loïc Pottier and Laurence Rideau. +Modifications by Lionel Elie Mamane for +generalising the protocol to suit other Coq interfaces. + The Pcoq Graphical Interface (see http://www-sop.inria.fr/lemme/pcoq) is developed by the Lemme team at INRIA Sophia-Antipolis (see http://www-sop.inria.fr/lemme) -- cgit v1.2.3