From 187dc15532f0c6f380d7bcb07adc2180c29fedc2 Mon Sep 17 00:00:00 2001
From: filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>
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
---
 theories/Sets/Classical_sets.v           | 7 +++++++
 theories/Sets/Constructive_sets.v        | 7 +++++++
 theories/Sets/Cpo.v                      | 7 +++++++
 theories/Sets/Ensembles.v                | 7 +++++++
 theories/Sets/Finite_sets.v              | 7 +++++++
 theories/Sets/Finite_sets_facts.v        | 7 +++++++
 theories/Sets/Image.v                    | 7 +++++++
 theories/Sets/Infinite_sets.v            | 7 +++++++
 theories/Sets/Integers.v                 | 7 +++++++
 theories/Sets/Multiset.v                 | 7 +++++++
 theories/Sets/Partial_Order.v            | 7 +++++++
 theories/Sets/Permut.v                   | 7 +++++++
 theories/Sets/Powerset.v                 | 7 +++++++
 theories/Sets/Powerset_Classical_facts.v | 7 +++++++
 theories/Sets/Powerset_facts.v           | 7 +++++++
 theories/Sets/Relations_1.v              | 7 +++++++
 theories/Sets/Relations_1_facts.v        | 7 +++++++
 theories/Sets/Relations_2.v              | 7 +++++++
 theories/Sets/Relations_2_facts.v        | 7 +++++++
 theories/Sets/Relations_3.v              | 7 +++++++
 theories/Sets/Relations_3_facts.v        | 7 +++++++
 theories/Sets/Uniset.v                   | 7 +++++++
 22 files changed, 154 insertions(+)

(limited to 'theories/Sets')

diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 2cd2df78a..0350f6114 100755
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 3c8023cae..03e6b5f01 100755
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index e367ac32b..7e828e75f 100755
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 68591b792..42cf98496 100755
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 5e721d8a0..0d1e9ff41 100755
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index b19fba44a..52ce9e651 100755
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index e7dc2184e..680b3f7fb 100755
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index b529775aa..02ea826f4 100755
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 21767405c..03572d760 100755
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index ae0d77035..5c37b0fd9 100755
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.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/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index a1c1639f0..0f117e62d 100755
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 8b4d0b7a4..baf28a53f 100755
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.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/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 9b2f57809..7caaacf97 100755
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 02a9b750d..bd46f6402 100755
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index b886f1211..4894ac486 100755
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 1e7e760a1..a7d1b3b17 100755
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 3c9609182..ddcc433b8 100755
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 28cc6a5f6..e0de488b8 100755
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 05f3753be..ec90057aa 100755
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 7b427aa5f..7e0f8ed26 100755
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index eec50c44f..3fe27af99 100755
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.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       *)
+(***********************************************************************)
 (****************************************************************************)
 (*                                                                          *)
 (*                         Naive Set Theory in Coq                          *)
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 5d9162fdb..b18b5634a 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.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$ *)
 
-- 
cgit v1.2.3