summaryrefslogtreecommitdiff
path: root/theories/Sets
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/Sets
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/Sets')
-rw-r--r--theories/Sets/Classical_sets.v4
-rw-r--r--theories/Sets/Constructive_sets.v4
-rw-r--r--theories/Sets/Cpo.v6
-rw-r--r--theories/Sets/Ensembles.v4
-rw-r--r--theories/Sets/Finite_sets.v4
-rw-r--r--theories/Sets/Finite_sets_facts.v8
-rw-r--r--theories/Sets/Image.v6
-rw-r--r--theories/Sets/Infinite_sets.v4
-rw-r--r--theories/Sets/Integers.v4
-rw-r--r--theories/Sets/Multiset.v4
-rw-r--r--theories/Sets/Partial_Order.v6
-rw-r--r--theories/Sets/Permut.v6
-rw-r--r--theories/Sets/Powerset.v6
-rw-r--r--theories/Sets/Powerset_Classical_facts.v4
-rw-r--r--theories/Sets/Powerset_facts.v4
-rw-r--r--theories/Sets/Relations_1.v6
-rw-r--r--theories/Sets/Relations_1_facts.v6
-rw-r--r--theories/Sets/Relations_2.v6
-rw-r--r--theories/Sets/Relations_2_facts.v6
-rw-r--r--theories/Sets/Relations_3.v4
-rw-r--r--theories/Sets/Relations_3_facts.v6
-rw-r--r--theories/Sets/Uniset.v6
22 files changed, 35 insertions, 79 deletions
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 701d9f8a..f93631c7 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Classical_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Require Export Constructive_sets.
Require Export Classical_Type.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index d3900446..e6dd8381 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Constructive_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Section Ensembles_facts.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index c7b496cb..d612e71e 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Cpo.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Require Export Relations_1.
Require Export Partial_Order.
@@ -107,4 +105,4 @@ Section Specific_orders.
{PO_of_chain : PO U;
Chain_cond : Totally_ordered U PO_of_chain (Carrier_of U PO_of_chain)}.
-End Specific_orders. \ No newline at end of file
+End Specific_orders.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 6c80ad40..58b979dd 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Ensembles.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Section Ensembles.
Variable U : Type.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index 09a0a94d..f0843675 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Finite_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Import Ensembles.
Section Ensembles_finis.
diff --git a/theories/Sets/Finite_sets_facts.v b/theories/Sets/Finite_sets_facts.v
index a9fe8ffe..350cd783 100644
--- a/theories/Sets/Finite_sets_facts.v
+++ b/theories/Sets/Finite_sets_facts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Finite_sets_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
@@ -175,14 +173,14 @@ Section Finite_sets_facts.
clear H'2 c2 Y.
intros X0 c2 H'2 H'3 x0 H'4 H'5.
elim (classic (In U X0 x)).
- intro H'6; apply f_equal with nat.
+ intro H'6; apply f_equal.
apply H'0 with (Y := Subtract U (Add U X0 x0) x).
elimtype (pred (S c2) = c2); auto with sets.
apply card_soustr_1; auto with sets.
rewrite <- H'5.
apply Sub_Add_new; auto with sets.
elim (classic (x = x0)).
- intros H'6 H'7; apply f_equal with nat.
+ intros H'6 H'7; apply f_equal.
apply H'0 with (Y := X0); auto with sets.
apply Simplify_add with (x := x); auto with sets.
pattern x at 2 in |- *; rewrite H'6; auto with sets.
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index e5eae17e..24facb6f 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Image.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
@@ -202,4 +200,4 @@ Section Image.
End Image.
-Hint Resolve Im_def image_empty finite_image: sets v62. \ No newline at end of file
+Hint Resolve Im_def image_empty finite_image: sets v62.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index afb9e0e1..a21fe880 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Infinite_sets.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v
index 5d073a0c..2c94a2e1 100644
--- a/theories/Sets/Integers.v
+++ b/theories/Sets/Integers.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Integers.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Finite_sets.
Require Export Constructive_sets.
Require Export Classical_Type.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 6187c08b..5f21335f 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Multiset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* G. Huet 1-9-95 *)
Require Import Permut Setoid.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index e819cafa..a319b983 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Partial_Order.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Require Export Relations_1.
@@ -99,4 +97,4 @@ Section Partial_order_facts.
apply Strict_Rel_Transitive_with_Rel with (y := y);
[ intuition | unfold Strict_Rel_of in H', H'0; intuition ].
Qed.
-End Partial_order_facts. \ No newline at end of file
+End Partial_order_facts.
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v
index 8699eed3..e28a1264 100644
--- a/theories/Sets/Permut.v
+++ b/theories/Sets/Permut.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Permut.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* G. Huet 1-9-95 *)
(** We consider a Set [U], given with a commutative-associative operator [op],
@@ -86,4 +84,4 @@ Section Axiomatisation.
apply cong_left; apply perm_left.
Qed.
-End Axiomatisation. \ No newline at end of file
+End Axiomatisation.
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 372473d6..f8b24e74 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Require Export Relations_1.
Require Export Relations_1_facts.
@@ -187,4 +185,4 @@ Hint Resolve Union_increases_r: sets v62.
Hint Resolve Intersection_decreases_l: sets v62.
Hint Resolve Intersection_decreases_r: sets v62.
Hint Resolve Empty_set_is_Bottom: sets v62.
-Hint Resolve Strict_inclusion_is_transitive: sets v62. \ No newline at end of file
+Hint Resolve Strict_inclusion_is_transitive: sets v62.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 66c0c0bb..09fc2094 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset_Classical_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Require Export Constructive_sets.
Require Export Relations_1.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 09edd08a..f756f985 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Powerset_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Ensembles.
Require Export Constructive_sets.
Require Export Relations_1.
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index 2818b370..a7fbb53d 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_1.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Section Relations_1.
Variable U : Type.
@@ -64,4 +62,4 @@ End Relations_1.
Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
same_relation: sets v62.
Hint Resolve Definition_of_preorder Definition_of_order
- Definition_of_equivalence Definition_of_PER: sets v62. \ No newline at end of file
+ Definition_of_equivalence Definition_of_PER: sets v62.
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index f002e926..0c8329dd 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_1_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Relations_1.
Definition Complement (U:Type) (R:Relation U) : Relation U :=
@@ -109,4 +107,4 @@ intros U R R' H' H'0; red in |- *.
elim H'.
intros H'1 H'2 x y z H'3 H'4; apply H'2.
apply H'0 with y; auto with sets.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 710bff2b..e7a69c99 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_2.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Relations_1.
Section Relations_2.
@@ -53,4 +51,4 @@ End Relations_2.
Hint Resolve Rstar_0: sets v62.
Hint Resolve Rstar1_0: sets v62.
Hint Resolve Rstar1_1: sets v62.
-Hint Resolve Rplus_0: sets v62. \ No newline at end of file
+Hint Resolve Rplus_0: sets v62.
diff --git a/theories/Sets/Relations_2_facts.v b/theories/Sets/Relations_2_facts.v
index 5ccdcb11..89b98c1f 100644
--- a/theories/Sets/Relations_2_facts.v
+++ b/theories/Sets/Relations_2_facts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_2_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Relations_2.
@@ -150,4 +148,4 @@ elim (H'3 t); auto with sets.
intros z1 H'5; elim H'5; intros H'8 H'10; try exact H'8; clear H'5.
exists z1; split; [ idtac | assumption ].
apply Rstar_n with t; auto with sets.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 1f96a75a..51092f7a 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_3.v 14641 2011-11-06 11:59:10Z 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 3a69a231..8ac6e7fb 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -24,8 +24,6 @@
(* in Summer 1995. Several developments by E. Ledinot were an inspiration. *)
(****************************************************************************)
-(*i $Id: Relations_3_facts.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Relations_2.
@@ -168,4 +166,4 @@ generalize (H'2 v); intro h; lapply h;
red in |- *; (exists z1; split); auto with sets.
apply T with y1; auto with sets.
apply T with t; auto with sets.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 48789f9a..bf1aaf8d 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Uniset.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(** Sets as characteristic functions *)
(* G. Huet 1-9-95 *)
@@ -212,4 +210,4 @@ i*)
End defs.
-Unset Implicit Arguments. \ No newline at end of file
+Unset Implicit Arguments.