diff options
author | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:15:08 -0400 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-08-06 16:17:55 -0400 |
commit | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (patch) | |
tree | c413c5bb42d20daf5307634ae6402526bb994fd6 /theories/Sets | |
parent | b9f47391f7f259c24119d1de0a87839e2cc5e80c (diff) |
Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg
Diffstat (limited to 'theories/Sets')
-rw-r--r-- | theories/Sets/Classical_sets.v | 2 | ||||
-rw-r--r-- | theories/Sets/Constructive_sets.v | 2 | ||||
-rw-r--r-- | theories/Sets/Cpo.v | 2 | ||||
-rw-r--r-- | theories/Sets/Ensembles.v | 2 | ||||
-rw-r--r-- | theories/Sets/Finite_sets.v | 2 | ||||
-rw-r--r-- | theories/Sets/Finite_sets_facts.v | 2 | ||||
-rw-r--r-- | theories/Sets/Image.v | 2 | ||||
-rw-r--r-- | theories/Sets/Infinite_sets.v | 2 | ||||
-rw-r--r-- | theories/Sets/Integers.v | 2 | ||||
-rw-r--r-- | theories/Sets/Multiset.v | 2 | ||||
-rw-r--r-- | theories/Sets/Partial_Order.v | 2 | ||||
-rw-r--r-- | theories/Sets/Permut.v | 2 | ||||
-rw-r--r-- | theories/Sets/Powerset.v | 2 | ||||
-rw-r--r-- | theories/Sets/Powerset_Classical_facts.v | 2 | ||||
-rw-r--r-- | theories/Sets/Powerset_facts.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_1.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_1_facts.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_2.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_2_facts.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_3.v | 2 | ||||
-rw-r--r-- | theories/Sets/Relations_3_facts.v | 2 | ||||
-rw-r--r-- | theories/Sets/Uniset.v | 2 |
22 files changed, 22 insertions, 22 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 824fd036..b20423e0 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Classical_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 8e0ab3b0..bb7235ff 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Constructive_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 0781781a..8591aef1 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Cpo.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index c96c21b4..1fee462d 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Ensembles.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Section Ensembles. Variable U : Type. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index cad440b4..f690e894 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Finite_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Import Ensembles. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index cc41a2ea..d351cc74 100644 --- a/theories/Sets/Finite_sets_facts.v +++ b/theories/Sets/Finite_sets_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Finite_sets_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index c48c844c..a58e12e6 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Image.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index 210205ed..c85cd8d2 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Infinite_sets.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 29208d03..37173094 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Integers.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 07fe2721..685a680f 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Multiset.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (* G. Huet 1-9-95 *) diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 95eb5102..671c9690 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Partial_Order.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index e1caff4f..844989c0 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Permut.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (* G. Huet 1-9-95 *) diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index b6df89f3..ae9dbb43 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Powerset.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index 93cb653a..f9da4816 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Powerset_Classical_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 7186881a..ab5bbaf9 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Powerset_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 54a5bd01..4677219e 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_1.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Section Relations_1. Variable U : Type. diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index a8d8209b..b6c0df25 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_1_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index e9cba979..9f7c831c 100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_2.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v index cbd596c3..039bae87 100644 --- a/theories/Sets/Relations_2_facts.v +++ b/theories/Sets/Relations_2_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_2_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. Require Export Relations_1_facts. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 99a68efc..d4a3d87c 100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_3.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. Require Export Relations_2. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index f85128ae..1a22aff9 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id$ i*) +(*i $Id: Relations_3_facts.v 13323 2010-07-24 15:57:30Z herbelin $ i*) Require Export Relations_1. Require Export Relations_1_facts. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 9803edc8..78da067d 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) +(*i $Id: Uniset.v 13323 2010-07-24 15:57:30Z herbelin $ i*) (** Sets as characteristic functions *) |