From 68d218a28a8ec0921997df6ac03ac23fe62f7993 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Thu, 7 Dec 2000 09:46:21 +0000 Subject: COPYRIGHT file added; some comments changed git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1080 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/COPYRIGHT | 13 +++++++++++++ contrib/xml/Xml.v | 4 ++-- contrib/xml/xml.mli | 4 ++-- contrib/xml/xmlcommand.ml | 6 ++---- contrib/xml/xmlcommand.mli | 4 ++-- contrib/xml/xmlentries.ml | 4 ++-- 6 files changed, 23 insertions(+), 12 deletions(-) create mode 100644 contrib/xml/COPYRIGHT (limited to 'contrib/xml') diff --git a/contrib/xml/COPYRIGHT b/contrib/xml/COPYRIGHT new file mode 100644 index 0000000000..a195efd5f2 --- /dev/null +++ b/contrib/xml/COPYRIGHT @@ -0,0 +1,13 @@ +This Coq module has been developed by Claudio Sacerdoti Coen + as a member of project HELM, to provide XML files +to be used in the project. +Project HELM (for Hypertextual Electronic Library of Mathematics) is a +project developed at the Department of Computer Science, University of Bologna; +http://www.cs.unibo.it/helm + +The author is interested in any other possible usage of the module. +So, if you plan to use the module in other projects/development, please +send him an e-mail. + +The licensing policy applied to the module is the same as for the whole Coq +distribution. diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v index adf195d942..5c6b788aa3 100644 --- a/contrib/xml/Xml.v +++ b/contrib/xml/Xml.v @@ -2,10 +2,10 @@ (* *) (* PROJECT HELM *) (* *) -(* A tactic to print Coq objects in XML *) +(* A module to print Coq objects in XML *) (* *) (* Claudio Sacerdoti Coen *) -(* 17/11/1999 *) +(* 06/12/2000 *) (******************************************************************************) Declare ML Module "xml" "xmlcommand" "xmlentries". diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli index a82c582f69..6f1dd08b35 100644 --- a/contrib/xml/xml.mli +++ b/contrib/xml/xml.mli @@ -2,10 +2,10 @@ (* *) (* PROJECT HELM *) (* *) -(* A tactic to print Coq objects in XML *) +(* A module to print Coq objects in XML *) (* *) (* Claudio Sacerdoti Coen *) -(* 18/10/2000 *) +(* 07/12/2000 *) (* *) (* This module defines a pretty-printer and the stream of commands to the pp *) (* *) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index f1cdd10198..4d85db397c 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -2,12 +2,10 @@ (* *) (* PROJECT HELM *) (* *) -(* A tactic to print Coq objects in XML *) +(* A module to print Coq objects in XML *) (* *) (* Claudio Sacerdoti Coen *) -(* 02/12/1999 *) -(* *) -(* This module defines the functions that implements the new commands *) +(* 06/12/2000 *) (* *) (******************************************************************************) diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 885873bfe4..84c71f0d7a 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -2,10 +2,10 @@ (* *) (* PROJECT HELM *) (* *) -(* A tactic to print Coq objects in XML *) +(* A module to print Coq objects in XML *) (* *) (* Claudio Sacerdoti Coen *) -(* 17/11/1999 *) +(* 07/12/2000 *) (* *) (* This module defines a pretty-printer and the stream of commands to the pp *) (* *) diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml index e6f792054d..ffa0d5fc79 100644 --- a/contrib/xml/xmlentries.ml +++ b/contrib/xml/xmlentries.ml @@ -2,10 +2,10 @@ (* *) (* PROJECT HELM *) (* *) -(* A tactic to print Coq objects in XML *) +(* A module to print Coq objects in XML *) (* *) (* Claudio Sacerdoti Coen *) -(* 18/10/2000 *) +(* 06/12/2000 *) (* *) (* This module adds to the vernacular interpreter the functions that fullfill *) (* the new commands defined in Xml.v *) -- cgit v1.2.3