aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--contrib/xml/acic.ml31
-rw-r--r--contrib/xml/acic2Xml.ml431
-rw-r--r--contrib/xml/cic2acic.ml31
-rw-r--r--contrib/xml/doubleTypeInference.ml31
-rw-r--r--contrib/xml/doubleTypeInference.mli31
-rw-r--r--contrib/xml/proof2aproof.ml30
-rw-r--r--contrib/xml/proofTree2Xml.ml431
-rw-r--r--contrib/xml/unshare.ml31
-rw-r--r--contrib/xml/unshare.mli31
-rw-r--r--contrib/xml/xml.ml432
-rw-r--r--contrib/xml/xml.mli31
-rw-r--r--contrib/xml/xmlcommand.ml32
-rw-r--r--contrib/xml/xmlcommand.mli31
-rw-r--r--contrib/xml/xmlentries.ml431
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*)