From 9fa3a718fca8a2b6e33630745812a891181cd052 Mon Sep 17 00:00:00 2001 From: sacerdot Date: Wed, 7 Apr 2004 23:18:26 +0000 Subject: Copyright notice of files in contrib/xml made uniform. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/xml/acic.ml | 33 ++++++++++++++++++++++++++++ contrib/xml/acic2Xml.ml4 | 12 +++++++++-- contrib/xml/cic2acic.ml | 33 ++++++++++++++++++++++++++++ contrib/xml/doubleTypeInference.ml | 39 ++++++++++++++++++++++----------- contrib/xml/doubleTypeInference.mli | 33 ++++++++++++++++++++++++++++ contrib/xml/proof2aproof.ml | 33 ++++++++++++++++++++++++++++ contrib/xml/proofTree2Xml.ml4 | 33 ++++++++++++++++++++++++++++ contrib/xml/unshare.ml | 39 ++++++++++++++++++++++----------- contrib/xml/unshare.mli | 39 ++++++++++++++++++++++----------- contrib/xml/xml.ml4 | 41 +++++++++++++++++++++++------------ contrib/xml/xml.mli | 41 +++++++++++++++++++++++------------ contrib/xml/xmlcommand.ml | 39 ++++++++++++++++++++++----------- contrib/xml/xmlcommand.mli | 41 +++++++++++++++++++++++------------ contrib/xml/xmlentries.ml4 | 43 ++++++++++++++++++++++++------------- 14 files changed, 392 insertions(+), 107 deletions(-) diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml index 36541a57df..461bd043b8 100644 --- a/contrib/xml/acic.ml +++ b/contrib/xml/acic.ml @@ -1,3 +1,36 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* *) -(* 22/06/2002 *) -(* *) -(*****************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) (*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *) type types = {synthesized : Term.types ; expected : Term.types option};; diff --git a/contrib/xml/doubleTypeInference.mli b/contrib/xml/doubleTypeInference.mli index a934eaa7e7..1db543acaa 100644 --- a/contrib/xml/doubleTypeInference.mli +++ b/contrib/xml/doubleTypeInference.mli @@ -1,3 +1,36 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* *) -(* 11/04/2002 *) -(* *) -(******************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) exception CanNotUnshare;; diff --git a/contrib/xml/unshare.mli b/contrib/xml/unshare.mli index 211258d276..5c2a345058 100644 --- a/contrib/xml/unshare.mli +++ b/contrib/xml/unshare.mli @@ -2,19 +2,34 @@ (* v * The Coq Proof Assistant / The Coq Development Team *) (* *) -(* 11/04/2002 *) -(* *) -(******************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) exception CanNotUnshare;; diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4 index ec2cd94759..7353acf42d 100644 --- a/contrib/xml/xml.ml4 +++ b/contrib/xml/xml.ml4 @@ -2,21 +2,34 @@ (* v * The Coq Proof Assistant / The Coq Development Team *) (* *) -(* 18/10/2000 *) -(* *) -(* This module defines a pretty-printer and the stream of commands to the pp *) -(* *) -(******************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) (* the type token for XML cdata, empty elements and not-empty elements *) diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli index fbdb584ee8..eb3f05e14c 100644 --- a/contrib/xml/xml.mli +++ b/contrib/xml/xml.mli @@ -2,21 +2,34 @@ (* v * The Coq Proof Assistant / The Coq Development Team *) (* *) -(* 07/12/2000 *) -(* *) -(* This module defines a pretty-printer and the stream of commands to the pp *) -(* *) -(******************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) (*i $Id$ i*) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 38c270db5a..24b1de09c0 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -2,19 +2,34 @@ (* v * The Coq Proof Assistant / The Coq Development Team *) (* *) -(* 22/06/2002 *) -(* *) -(*****************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) (* CONFIGURATION PARAMETERS *) diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index dd5fce636b..04a894feee 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -2,21 +2,34 @@ (* v * The Coq Proof Assistant / The Coq Development Team *) (* *) -(* 07/12/2000 *) -(* *) -(* This module defines a pretty-printer and the stream of commands to the pp *) -(* *) -(******************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) (*i $Id$ i*) diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index 6de9411288..8356d670e4 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -2,22 +2,35 @@ (* v * The Coq Proof Assistant / The Coq Development Team *) (* *) -(* 06/12/2000 *) -(* *) -(* This module adds to the vernacular interpreter the functions that fullfill *) -(* the new commands defined in Xml.v *) -(* *) -(******************************************************************************) + +(* Copyright (C) 2000-2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://helm.unibo.it/. + *) + (*i camlp4deps: "parsing/grammar.cma" i*) (* $Id$ *) -- cgit v1.2.3