diff options
| -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 0000000000..a195efd5f2 --- /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 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 <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 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 <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 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 <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 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 <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 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 <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 *) |