From 187dc15532f0c6f380d7bcb07adc2180c29fedc2 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 15 Mar 2001 13:38:59 +0000
Subject: entetes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/Extraction.v      | 7 +++++++
 contrib/extraction/close_env.ml      | 7 +++++++
 contrib/extraction/close_env.mli     | 7 +++++++
 contrib/extraction/extraction.ml     | 7 +++++++
 contrib/extraction/extraction.mli    | 7 +++++++
 contrib/extraction/genpp.ml          | 7 +++++++
 contrib/extraction/genpp.mli         | 7 +++++++
 contrib/extraction/miniml.mli        | 7 +++++++
 contrib/extraction/mlimport.ml       | 7 +++++++
 contrib/extraction/mlimport.mli      | 7 +++++++
 contrib/extraction/ocaml.ml          | 7 +++++++
 contrib/extraction/ocaml.mli         | 7 +++++++
 contrib/extraction/test_extraction.v | 7 +++++++
 contrib/omega/Omega.v                | 7 +++++++
 contrib/omega/OmegaSyntax.v          | 7 +++++++
 contrib/omega/Zcomplements.v         | 7 +++++++
 contrib/omega/Zlogarithm.v           | 7 +++++++
 contrib/omega/Zpower.v               | 7 +++++++
 contrib/omega/coq_omega.ml           | 7 +++++++
 contrib/omega/omega.ml               | 7 +++++++
 contrib/ring/ArithRing.v             | 7 +++++++
 contrib/ring/Quote.v                 | 7 +++++++
 contrib/ring/Ring.v                  | 7 +++++++
 contrib/ring/Ring_abstract.v         | 7 +++++++
 contrib/ring/Ring_normalize.v        | 7 +++++++
 contrib/ring/Ring_theory.v           | 7 +++++++
 contrib/ring/ZArithRing.v            | 7 +++++++
 contrib/ring/quote.ml                | 7 +++++++
 contrib/ring/ring.ml                 | 7 +++++++
 contrib/xml/Xml.v                    | 7 +++++++
 contrib/xml/xml.ml                   | 7 +++++++
 contrib/xml/xml.mli                  | 7 +++++++
 contrib/xml/xmlcommand.ml            | 7 +++++++
 contrib/xml/xmlcommand.mli           | 7 +++++++
 contrib/xml/xmlentries.ml            | 7 +++++++
 35 files changed, 245 insertions(+)

(limited to 'contrib')

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 9e0f23c2d0..0f9668756c 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 Declare ML Module "ocaml.cmo" "extraction.cmo".
 
diff --git a/contrib/extraction/close_env.ml b/contrib/extraction/close_env.ml
index 2b4c66da6c..ab303b0947 100644
--- a/contrib/extraction/close_env.ml
+++ b/contrib/extraction/close_env.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/close_env.mli b/contrib/extraction/close_env.mli
index 066bb2a6d1..bf6940d1cc 100644
--- a/contrib/extraction/close_env.mli
+++ b/contrib/extraction/close_env.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a6f46235b0..6aa5b7977c 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 4c1d492c17..df5a414a1f 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/genpp.ml b/contrib/extraction/genpp.ml
index 27390de44f..55d80d8467 100644
--- a/contrib/extraction/genpp.ml
+++ b/contrib/extraction/genpp.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/genpp.mli b/contrib/extraction/genpp.mli
index 1bd795c090..376b069d0d 100644
--- a/contrib/extraction/genpp.mli
+++ b/contrib/extraction/genpp.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 525b8dc3d9..95b81fe108 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/mlimport.ml b/contrib/extraction/mlimport.ml
index 12e39d0441..6fd5d86571 100644
--- a/contrib/extraction/mlimport.ml
+++ b/contrib/extraction/mlimport.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/mlimport.mli b/contrib/extraction/mlimport.mli
index 6e302989fe..4fdb2e9eae 100644
--- a/contrib/extraction/mlimport.mli
+++ b/contrib/extraction/mlimport.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index ba7d59e724..83189ec579 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index be80e419a6..ff8dce97fe 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index 2f06ad3972..2d40d97f52 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 Extraction nat.
 
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 8c646ae087..6c4a6191b5 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (**************************************************************************)
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
diff --git a/contrib/omega/OmegaSyntax.v b/contrib/omega/OmegaSyntax.v
index af673b097d..a7f67f1815 100644
--- a/contrib/omega/OmegaSyntax.v
+++ b/contrib/omega/OmegaSyntax.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (**************************************************************************)
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
diff --git a/contrib/omega/Zcomplements.v b/contrib/omega/Zcomplements.v
index c808232371..52607a4a0d 100644
--- a/contrib/omega/Zcomplements.v
+++ b/contrib/omega/Zcomplements.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v
index 5d343880e0..3d29e0503f 100644
--- a/contrib/omega/Zlogarithm.v
+++ b/contrib/omega/Zlogarithm.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index 824012d124..c2585b3e08 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 821c4b2021..71bfbe290a 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (**************************************************************************)
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml
index 86f1a2e334..6d78494a22 100755
--- a/contrib/omega/omega.ml
+++ b/contrib/omega/omega.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (**************************************************************************)
 (*                                                                        *)
 (* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index 14d69e2b02..0dfb1f4e35 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index e7c995cf3b..f97c81c408 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index b6f75a5841..c94dce065e 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index 6bb1f5aa9a..7626899850 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 536d2d3034..94b5093c70 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index c04eee57ec..867ab22fbe 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/ZArithRing.v b/contrib/ring/ZArithRing.v
index a8adfe2f63..2de8611764 100644
--- a/contrib/ring/ZArithRing.v
+++ b/contrib/ring/ZArithRing.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index ac3af30b8d..c82ccecb00 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 0e200313c7..589c1580ea 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/contrib/xml/Xml.v b/contrib/xml/Xml.v
index 5c6b788aa3..f1d91371e9 100644
--- a/contrib/xml/Xml.v
+++ b/contrib/xml/Xml.v
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
diff --git a/contrib/xml/xml.ml b/contrib/xml/xml.ml
index 635e83f68a..60e16ab19b 100644
--- a/contrib/xml/xml.ml
+++ b/contrib/xml/xml.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli
index 0510d978da..fbdb584ee8 100644
--- a/contrib/xml/xml.mli
+++ b/contrib/xml/xml.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 906cf8b078..3927827276 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 1c9b22070a..0ddc01c9a4 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
diff --git a/contrib/xml/xmlentries.ml b/contrib/xml/xmlentries.ml
index ffa0d5fc79..093727f2f1 100644
--- a/contrib/xml/xmlentries.ml
+++ b/contrib/xml/xmlentries.ml
@@ -1,3 +1,10 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
 (******************************************************************************)
 (*                                                                            *)
 (*                               PROJECT HELM                                 *)
-- 
cgit v1.2.3