diff options
-rw-r--r-- | contrib/xml/acic.ml | 31 | ||||
-rw-r--r-- | contrib/xml/acic2Xml.ml4 | 31 | ||||
-rw-r--r-- | contrib/xml/cic2acic.ml | 31 | ||||
-rw-r--r-- | contrib/xml/doubleTypeInference.ml | 31 | ||||
-rw-r--r-- | contrib/xml/doubleTypeInference.mli | 31 | ||||
-rw-r--r-- | contrib/xml/proof2aproof.ml | 30 | ||||
-rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 31 | ||||
-rw-r--r-- | contrib/xml/unshare.ml | 31 | ||||
-rw-r--r-- | contrib/xml/unshare.mli | 31 | ||||
-rw-r--r-- | contrib/xml/xml.ml4 | 32 | ||||
-rw-r--r-- | contrib/xml/xml.mli | 31 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.ml | 32 | ||||
-rw-r--r-- | contrib/xml/xmlcommand.mli | 31 | ||||
-rw-r--r-- | contrib/xml/xmlentries.ml4 | 31 |
14 files changed, 84 insertions, 351 deletions
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml index 461bd043b..e1bfe866a 100644 --- a/contrib/xml/acic.ml +++ b/contrib/xml/acic.ml @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) open Names open Term diff --git a/contrib/xml/acic2Xml.ml4 b/contrib/xml/acic2Xml.ml4 index bb2f59ee0..c1715bfc3 100644 --- a/contrib/xml/acic2Xml.ml4 +++ b/contrib/xml/acic2Xml.ml4 @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) (*CSC codice cut & paste da cicPp e xmlcommand *) diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index 20f05b575..a6b2eaf00 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) (* Utility Functions *) diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 3da92d0fd..3c5362509 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.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 1db543aca..501a149e7 100644 --- a/contrib/xml/doubleTypeInference.mli +++ b/contrib/xml/doubleTypeInference.mli @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) type types = { synthesized : Term.types; expected : Term.types option; } diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index de86ce341..304aed89e 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -5,31 +5,13 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) -(* 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/. - *) (* Note: we can not use the Set module here because we _need_ physical *) (* equality and there exists no comparison function compatible with *) (* physical equality. *) diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index a4baaea54..aaf8cec72 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";; diff --git a/contrib/xml/unshare.ml b/contrib/xml/unshare.ml index e12cd865e..131a2f5a1 100644 --- a/contrib/xml/unshare.ml +++ b/contrib/xml/unshare.ml @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) exception CanNotUnshare;; diff --git a/contrib/xml/unshare.mli b/contrib/xml/unshare.mli index 5c2a34505..eaab1c38c 100644 --- a/contrib/xml/unshare.mli +++ b/contrib/xml/unshare.mli @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) exception CanNotUnshare;; diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4 index 7353acf42..b9de14e7e 100644 --- a/contrib/xml/xml.ml4 +++ b/contrib/xml/xml.ml4 @@ -5,32 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) - +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) (* the type token for XML cdata, empty elements and not-empty elements *) (* Usage: *) diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli index eb3f05e14..d10894fc2 100644 --- a/contrib/xml/xml.mli +++ b/contrib/xml/xml.mli @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 24b1de09c..3004f39e9 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -5,32 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) - +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) (* CONFIGURATION PARAMETERS *) diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli index 04a894fee..35a3c5e63 100644 --- a/contrib/xml/xmlcommand.mli +++ b/contrib/xml/xmlcommand.mli @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) (*i $Id$ i*) diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4 index 8356d670e..22639d662 100644 --- a/contrib/xml/xmlentries.ml4 +++ b/contrib/xml/xmlentries.ml4 @@ -5,31 +5,12 @@ (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) (***********************************************************************) - -(* 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/. - *) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(***********************************************************************) (*i camlp4deps: "parsing/grammar.cma" i*) |