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
---
 lib/bij.ml         | 7 +++++++
 lib/bij.mli        | 7 +++++++
 lib/bstack.ml      | 7 +++++++
 lib/bstack.mli     | 7 +++++++
 lib/dyn.ml         | 7 +++++++
 lib/dyn.mli        | 7 +++++++
 lib/edit.ml        | 7 +++++++
 lib/edit.mli       | 7 +++++++
 lib/explore.ml     | 7 +++++++
 lib/explore.mli    | 7 +++++++
 lib/gmap.ml        | 7 +++++++
 lib/gmap.mli       | 7 +++++++
 lib/gmapl.ml       | 7 +++++++
 lib/gmapl.mli      | 7 +++++++
 lib/gset.ml        | 7 +++++++
 lib/gset.mli       | 7 +++++++
 lib/hashcons.ml    | 7 +++++++
 lib/hashcons.mli   | 7 +++++++
 lib/options.ml     | 7 +++++++
 lib/options.mli    | 7 +++++++
 lib/pp.ml          | 7 +++++++
 lib/pp.mli         | 7 +++++++
 lib/pp_control.ml  | 7 +++++++
 lib/pp_control.mli | 7 +++++++
 lib/profile.ml     | 7 +++++++
 lib/profile.mli    | 7 +++++++
 lib/stamps.ml      | 7 +++++++
 lib/stamps.mli     | 7 +++++++
 lib/system.ml      | 7 +++++++
 lib/system.mli     | 7 +++++++
 lib/tlm.ml         | 7 +++++++
 lib/tlm.mli        | 7 +++++++
 lib/util.ml        | 7 +++++++
 lib/util.mli       | 7 +++++++
 34 files changed, 238 insertions(+)

(limited to 'lib')

diff --git a/lib/bij.ml b/lib/bij.ml
index cd0acbabbb..345867f34b 100644
--- a/lib/bij.ml
+++ b/lib/bij.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/lib/bij.mli b/lib/bij.mli
index 7e6d23e828..e67db5364c 100644
--- a/lib/bij.mli
+++ b/lib/bij.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/lib/bstack.ml b/lib/bstack.ml
index c67f51092c..c52b0e713a 100644
--- a/lib/bstack.ml
+++ b/lib/bstack.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/lib/bstack.mli b/lib/bstack.mli
index fc646f1a4f..febf7850ed 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.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/lib/dyn.ml b/lib/dyn.ml
index 3d6d43f8c4..0bbf773b9b 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.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/lib/dyn.mli b/lib/dyn.mli
index 2c0587ee67..819f240b9e 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.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/lib/edit.ml b/lib/edit.ml
index 8d0b0aa276..ca41a04365 100644
--- a/lib/edit.ml
+++ b/lib/edit.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/lib/edit.mli b/lib/edit.mli
index c86022e443..4f3b7803c1 100644
--- a/lib/edit.mli
+++ b/lib/edit.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/lib/explore.ml b/lib/explore.ml
index b79f3e8207..47a6687e5d 100644
--- a/lib/explore.ml
+++ b/lib/explore.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/lib/explore.mli b/lib/explore.mli
index 5f484f8e6a..6350feccba 100644
--- a/lib/explore.mli
+++ b/lib/explore.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/lib/gmap.ml b/lib/gmap.ml
index 52af882b35..83a8cc3d69 100644
--- a/lib/gmap.ml
+++ b/lib/gmap.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$ *)
 
 (* Maps using the generic comparison function of ocaml. Code borrowed from
diff --git a/lib/gmap.mli b/lib/gmap.mli
index a73bdba519..107e5e2d99 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.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/lib/gmapl.ml b/lib/gmapl.ml
index 6295c4099c..013b91ac34 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.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/lib/gmapl.mli b/lib/gmapl.mli
index 23c77851bc..f44fad27c0 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.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/lib/gset.ml b/lib/gset.ml
index 1dc710be0b..e18e01187f 100644
--- a/lib/gset.ml
+++ b/lib/gset.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/lib/gset.mli b/lib/gset.mli
index 125fbe4422..f6f2a95eaa 100644
--- a/lib/gset.mli
+++ b/lib/gset.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/lib/hashcons.ml b/lib/hashcons.ml
index 55405a7aaf..45ef9a0f53 100644
--- a/lib/hashcons.ml
+++ b/lib/hashcons.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/lib/hashcons.mli b/lib/hashcons.mli
index 07dd8bc2b0..aea23900b1 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.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/lib/options.ml b/lib/options.ml
index a4e00c6b37..82ee767d34 100644
--- a/lib/options.ml
+++ b/lib/options.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/lib/options.mli b/lib/options.mli
index 576794f39c..61372bfe5e 100644
--- a/lib/options.mli
+++ b/lib/options.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/lib/pp.ml b/lib/pp.ml
index d29eaf6f1f..bee373aa07 100644
--- a/lib/pp.ml
+++ b/lib/pp.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/lib/pp.mli b/lib/pp.mli
index 96ef3d3ded..d0730044c1 100644
--- a/lib/pp.mli
+++ b/lib/pp.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/lib/pp_control.ml b/lib/pp_control.ml
index 34ebf76fc5..2e84767901 100644
--- a/lib/pp_control.ml
+++ b/lib/pp_control.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/lib/pp_control.mli b/lib/pp_control.mli
index b6d6132e01..2551726df3 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.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/lib/profile.ml b/lib/profile.ml
index 8a90abf5de..825b792d7d 100644
--- a/lib/profile.ml
+++ b/lib/profile.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/lib/profile.mli b/lib/profile.mli
index 647aaea44c..8d4105cf6a 100644
--- a/lib/profile.mli
+++ b/lib/profile.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       *)
+(***********************************************************************)
 
 (* $Id$ *)
 
diff --git a/lib/stamps.ml b/lib/stamps.ml
index 0441d2de16..ab1b608a54 100644
--- a/lib/stamps.ml
+++ b/lib/stamps.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/lib/stamps.mli b/lib/stamps.mli
index 40a83feb69..a85d7174d3 100644
--- a/lib/stamps.mli
+++ b/lib/stamps.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/lib/system.ml b/lib/system.ml
index db478d9e35..cf48f0e4b4 100644
--- a/lib/system.ml
+++ b/lib/system.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/lib/system.mli b/lib/system.mli
index a9ffd5b63e..5c893eb30e 100644
--- a/lib/system.mli
+++ b/lib/system.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/lib/tlm.ml b/lib/tlm.ml
index d16353f1ec..fca2db5ec7 100644
--- a/lib/tlm.ml
+++ b/lib/tlm.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/lib/tlm.mli b/lib/tlm.mli
index f046397504..1a6f611241 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.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/lib/util.ml b/lib/util.ml
index 29273b1690..5e10091e3f 100644
--- a/lib/util.ml
+++ b/lib/util.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/lib/util.mli b/lib/util.mli
index 274d97af41..d46672a603 100644
--- a/lib/util.mli
+++ b/lib/util.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*)
 
-- 
cgit v1.2.3