aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Sets
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-15 13:38:59 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-15 13:38:59 +0000
commit187dc15532f0c6f380d7bcb07adc2180c29fedc2 (patch)
treed7bacf01519ca82b5745d2c493c7f7f1826106af /theories/Sets
parent23741168b109daece8bb588b9c5fb4506e7726ce (diff)
entetes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Sets')
-rwxr-xr-xtheories/Sets/Classical_sets.v7
-rwxr-xr-xtheories/Sets/Constructive_sets.v7
-rwxr-xr-xtheories/Sets/Cpo.v7
-rwxr-xr-xtheories/Sets/Ensembles.v7
-rwxr-xr-xtheories/Sets/Finite_sets.v7
-rwxr-xr-xtheories/Sets/Finite_sets_facts.v7
-rwxr-xr-xtheories/Sets/Image.v7
-rwxr-xr-xtheories/Sets/Infinite_sets.v7
-rwxr-xr-xtheories/Sets/Integers.v7
-rwxr-xr-xtheories/Sets/Multiset.v7
-rwxr-xr-xtheories/Sets/Partial_Order.v7
-rwxr-xr-xtheories/Sets/Permut.v7
-rwxr-xr-xtheories/Sets/Powerset.v7
-rwxr-xr-xtheories/Sets/Powerset_Classical_facts.v7
-rwxr-xr-xtheories/Sets/Powerset_facts.v7
-rwxr-xr-xtheories/Sets/Relations_1.v7
-rwxr-xr-xtheories/Sets/Relations_1_facts.v7
-rwxr-xr-xtheories/Sets/Relations_2.v7
-rwxr-xr-xtheories/Sets/Relations_2_facts.v7
-rwxr-xr-xtheories/Sets/Relations_3.v7
-rwxr-xr-xtheories/Sets/Relations_3_facts.v7
-rw-r--r--theories/Sets/Uniset.v7
22 files changed, 154 insertions, 0 deletions
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$ *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 14:37:44 +0000