diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-07 09:46:21 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-07 09:46:21 +0000 |
| commit | 68d218a28a8ec0921997df6ac03ac23fe62f7993 (patch) | |
| tree | c2074cfc89aec051f6ee8d6f04671ec6c74ad041 /contrib | |
| parent | a39d9579cb2a227a49d23ae68d4f61f5d24b65f7 (diff) | |
COPYRIGHT file added; some comments changed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1080 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/xml/COPYRIGHT | 13 | ||||
| -rw-r--r-- | contrib/xml/Xml.v | 4 | ||||
| -rw-r--r-- | contrib/xml/xml.mli | 4 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 6 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.mli | 4 | ||||
| -rw-r--r-- | contrib/xml/xmlentries.ml | 4 |
6 files changed, 23 insertions, 12 deletions
diff --git a/contrib/xml/COPYRIGHT b/contrib/xml/COPYRIGHT new file mode 100644 index 000000000..a195efd5f --- /dev/null +++ b/contrib/xml/COPYRIGHT @@ -0,0 +1,13 @@ +This Coq module has been developed by Claudio Sacerdoti Coen +<sacerdot@cs.unibo.it> 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 adf195d94..5c6b788aa 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 <sacerdot@cs.unibo.it> *) -(* 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 a82c582f6..6f1dd08b3 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 <sacerdot@cs.unibo.it> *) -(* 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 f1cdd1019..4d85db397 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 <sacerdot@cs.unibo.it> *) -(* 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 885873bfe..84c71f0d7 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 <sacerdot@cs.unibo.it> *) -(* 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 e6f792054..ffa0d5fc7 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 <sacerdot@cs.unibo.it> *) -(* 18/10/2000 *) +(* 06/12/2000 *) (* *) (* This module adds to the vernacular interpreter the functions that fullfill *) (* the new commands defined in Xml.v *) |