From 91c7cb8fb1a924e1e924195724720b81d777d8a9 Mon Sep 17 00:00:00 2001 From: mohring Date: Thu, 19 Apr 2001 12:48:37 +0000 Subject: Mise de (*i autour CVS info git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1622 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Sets/Classical_sets.v | 2 +- theories/Sets/Constructive_sets.v | 2 +- theories/Sets/Cpo.v | 2 +- theories/Sets/Ensembles.v | 2 +- theories/Sets/Finite_sets.v | 2 +- theories/Sets/Finite_sets_facts.v | 2 +- theories/Sets/Image.v | 2 +- theories/Sets/Infinite_sets.v | 2 +- theories/Sets/Integers.v | 2 +- theories/Sets/Multiset.v | 2 +- theories/Sets/Partial_Order.v | 2 +- theories/Sets/Permut.v | 2 +- theories/Sets/Powerset.v | 2 +- theories/Sets/Powerset_Classical_facts.v | 2 +- theories/Sets/Powerset_facts.v | 2 +- theories/Sets/Relations_1.v | 2 +- theories/Sets/Relations_2.v | 2 +- theories/Sets/Relations_3.v | 2 ++ 18 files changed, 19 insertions(+), 17 deletions(-) (limited to 'theories/Sets') diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 0350f6114..cd72483a3 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 03e6b5f01..9d24ae433 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Ensembles. diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index 7e828e75f..c234bd1c7 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index d92865c5d..0ddad8578 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Section Ensembles. Variable U: Type. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index 0d1e9ff41..1e0c05450 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Ensembles. diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v index 52ce9e651..0f11b389a 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 680b3f7fb..db41d6ac6 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index 02ea826f4..c6233453a 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 03572d760..85d3b1c12 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Finite_sets. Require Export Constructive_sets. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index cd7b1e23e..9e79ee3a0 100755 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (* G. Huet 1-9-95 *) diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 0f117e62d..f3d692b85 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Ensembles. Require Export Relations_1. diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index e19f73a8c..686ea973e 100755 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(* $Id$ *) +(*i $Id$ i*) (* G. Huet 1-9-95 *) diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 7caaacf97..c9c7188b1 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ 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 bd46f6402..6b3443b7d 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 4894ac486..699c5f362 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Ensembles. Require Export Constructive_sets. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index a7d1b3b17..74c031726 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Section Relations_1. Variable U: Type. diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index e0de488b8..65363d816 100755 --- 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. *) (****************************************************************************) -(* $Id$ *) +(*i $Id$ i*) Require Export Relations_1. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 7e0f8ed26..9bd6e8e5b 100755 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -24,6 +24,8 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) +(*i $Id$ *i) + Require Export Relations_1. Require Export Relations_2. -- cgit v1.2.3