aboutsummaryrefslogtreecommitdiff
path: root/contrib/xml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml')
-rw-r--r--contrib/xml/acic.ml26
-rw-r--r--contrib/xml/acic2Xml.ml426
-rw-r--r--contrib/xml/cic2acic.ml26
-rw-r--r--contrib/xml/doubleTypeInference.ml26
-rw-r--r--contrib/xml/doubleTypeInference.mli26
-rw-r--r--contrib/xml/proof2aproof.ml26
-rw-r--r--contrib/xml/proofTree2Xml.ml426
-rw-r--r--contrib/xml/unshare.ml26
-rw-r--r--contrib/xml/unshare.mli26
-rw-r--r--contrib/xml/xml.ml426
-rw-r--r--contrib/xml/xml.mli26
-rw-r--r--contrib/xml/xmlcommand.ml26
-rw-r--r--contrib/xml/xmlcommand.mli26
-rw-r--r--contrib/xml/xmlentries.ml426
14 files changed, 182 insertions, 182 deletions
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml
index e1bfe866a7..032ddbebe0 100644
--- a/contrib/xml/acic.ml
+++ b/contrib/xml/acic.ml
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
open Names
open Term
diff --git a/contrib/xml/acic2Xml.ml4 b/contrib/xml/acic2Xml.ml4
index c1715bfc3c..64dc8a0503 100644
--- a/contrib/xml/acic2Xml.ml4
+++ b/contrib/xml/acic2Xml.ml4
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(*CSC codice cut & paste da cicPp e xmlcommand *)
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 4809e443ce..d820f9e594 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(* Utility Functions *)
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 3c53625090..f0e3f5e356 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(*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 501a149e7e..33d3e5cd03 100644
--- a/contrib/xml/doubleTypeInference.mli
+++ b/contrib/xml/doubleTypeInference.mli
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
type types = { synthesized : Term.types; expected : Term.types option; }
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml
index 304aed89e6..165a456dca 100644
--- a/contrib/xml/proof2aproof.ml
+++ b/contrib/xml/proof2aproof.ml
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(* Note: we can not use the Set module here because we _need_ physical *)
(* equality and there exists no comparison function compatible with *)
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index aaf8cec729..b9b66774a5 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
let prooftreedtdname = "http://mowgli.cs.unibo.it/dtd/prooftree.dtd";;
diff --git a/contrib/xml/unshare.ml b/contrib/xml/unshare.ml
index 131a2f5a11..f30f8230de 100644
--- a/contrib/xml/unshare.ml
+++ b/contrib/xml/unshare.ml
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
exception CanNotUnshare;;
diff --git a/contrib/xml/unshare.mli b/contrib/xml/unshare.mli
index eaab1c38cc..31ba90372e 100644
--- a/contrib/xml/unshare.mli
+++ b/contrib/xml/unshare.mli
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
exception CanNotUnshare;;
diff --git a/contrib/xml/xml.ml4 b/contrib/xml/xml.ml4
index b9de14e7e6..d0c64f309f 100644
--- a/contrib/xml/xml.ml4
+++ b/contrib/xml/xml.ml4
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(* 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 d10894fc27..fdb84ebcb8 100644
--- a/contrib/xml/xml.mli
+++ b/contrib/xml/xml.mli
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(*i $Id$ i*)
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 586a208755..2157dab56f 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(* CONFIGURATION PARAMETERS *)
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 35a3c5e638..66ff9f0bbd 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(*i $Id$ i*)
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
index 22639d6620..41c107ad2c 100644
--- a/contrib/xml/xmlentries.ml4
+++ b/contrib/xml/xmlentries.ml4
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * 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 *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * 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 *)
+(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 04:08:39 +0000