Mise de (*i autour CVS info

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1622 85f007b7-540e-0410-9357-904b9bb8a0f7

18 files changed, 19 insertions, 17 deletions

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.