aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xtheories/Sets/Classical_sets.v2
-rwxr-xr-xtheories/Sets/Constructive_sets.v2
-rwxr-xr-xtheories/Sets/Cpo.v2
-rwxr-xr-xtheories/Sets/Ensembles.v2
-rwxr-xr-xtheories/Sets/Finite_sets.v2
-rwxr-xr-xtheories/Sets/Finite_sets_facts.v2
-rwxr-xr-xtheories/Sets/Image.v2
-rwxr-xr-xtheories/Sets/Infinite_sets.v2
-rwxr-xr-xtheories/Sets/Integers.v2
-rwxr-xr-xtheories/Sets/Multiset.v2
-rwxr-xr-xtheories/Sets/Partial_Order.v2
-rwxr-xr-xtheories/Sets/Permut.v2
-rwxr-xr-xtheories/Sets/Powerset.v2
-rwxr-xr-xtheories/Sets/Powerset_Classical_facts.v2
-rwxr-xr-xtheories/Sets/Powerset_facts.v2
-rwxr-xr-xtheories/Sets/Relations_1.v2
-rwxr-xr-xtheories/Sets/Relations_2.v2
-rwxr-xr-xtheories/Sets/Relations_3.v2
18 files changed, 19 insertions, 17 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 0350f61147..cd72483a31 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 03e6b5f01a..9d24ae433b 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 7e828e75f0..c234bd1c74 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 d92865c5d7..0ddad85787 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 0d1e9ff41a..1e0c05450e 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 52ce9e6512..0f11b389a3 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 680b3f7fb4..db41d6ac68 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 02ea826f4b..c6233453a8 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 03572d7606..85d3b1c124 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 cd7b1e23e4..9e79ee3a0c 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 0f117e62db..f3d692b85b 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 e19f73a8c1..686ea973e0 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 7caaacf97a..c9c7188b1a 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 bd46f64025..6b3443b7d5 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 4894ac4867..699c5f3628 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 a7d1b3b179..74c0317265 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 e0de488b8f..65363d8164 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 7e0f8ed26f..9bd6e8e5bc 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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:21:05 +0000