summaryrefslogtreecommitdiff
path: root/theories/Sets
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Sets')
-rw-r--r--theories/Sets/Classical_sets.v2
-rw-r--r--theories/Sets/Constructive_sets.v2
-rw-r--r--theories/Sets/Cpo.v2
-rw-r--r--theories/Sets/Ensembles.v2
-rw-r--r--theories/Sets/Finite_sets.v2
-rw-r--r--theories/Sets/Finite_sets_facts.v2
-rw-r--r--theories/Sets/Image.v2
-rw-r--r--theories/Sets/Infinite_sets.v2
-rw-r--r--theories/Sets/Integers.v2
-rw-r--r--theories/Sets/Multiset.v2
-rw-r--r--theories/Sets/Partial_Order.v2
-rw-r--r--theories/Sets/Permut.v2
-rw-r--r--theories/Sets/Powerset.v2
-rw-r--r--theories/Sets/Powerset_Classical_facts.v2
-rw-r--r--theories/Sets/Powerset_facts.v2
-rw-r--r--theories/Sets/Relations_1.v2
-rw-r--r--theories/Sets/Relations_1_facts.v2
-rw-r--r--theories/Sets/Relations_2.v2
-rw-r--r--theories/Sets/Relations_2_facts.v2
-rw-r--r--theories/Sets/Relations_3.v2
-rw-r--r--theories/Sets/Relations_3_facts.v2
-rw-r--r--theories/Sets/Uniset.v2
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 11:48:18 +0000