Imported Upstream version 8.4dfsgupstream/8.4dfsg

4 files changed, 13 insertions, 13 deletions

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index f7f5512e..779c3d9a 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -50,7 +50,7 @@ Section Properties.
 
     Lemma clos_rt_idempotent : inclusion (R*)* R*.
     Proof.
-      red in |- *.
+      red.
       induction 1; auto with sets.
       intros.
       apply rt_trans with y; auto with sets.
@@ -66,7 +66,7 @@ Section Properties.
     Lemma clos_rt_clos_rst :
       inclusion (clos_refl_trans R) (clos_refl_sym_trans R).
     Proof.
-      red in |- *.
+      red.
       induction 1; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
@@ -87,7 +87,7 @@ Section Properties.
       inclusion (clos_refl_sym_trans (clos_refl_sym_trans R))
       (clos_refl_sym_trans R).
     Proof.
-      red in |- *.
+      red.
       induction 1; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index a84c1310..0e6d034e 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index abf23997..b7159578 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -149,13 +149,13 @@ Section Lexicographic_Product.
   Variable leA : A -> A -> Prop.
   Variable leB : forall x:A, B x -> B x -> Prop.
 
-  Inductive lexprod : sigS B -> sigS B -> Prop :=
+  Inductive lexprod : sigT B -> sigT B -> Prop :=
     | left_lex :
       forall (x x':A) (y:B x) (y':B x'),
-        leA x x' -> lexprod (existS B x y) (existS B x' y')
+        leA x x' -> lexprod (existT B x y) (existT B x' y')
     | right_lex :
       forall (x:A) (y y':B x),
-        leB x y y' -> lexprod (existS B x y) (existS B x y').
+        leB x y y' -> lexprod (existT B x y) (existT B x y').
 
 End Lexicographic_Product.
 
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index f9fb2c44..08b7574f 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -14,16 +14,16 @@ Lemma inverse_image_of_equivalence :
   forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
 Proof.
-  intros; split; elim H; red in |- *; auto.
+  intros; split; elim H; red; auto.
   intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
 Lemma inverse_image_of_eq :
   forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.
-  split; red in |- *;
+  split; red;
     [  (* reflexivity *) reflexivity
       |  (* transitivity *) intros; transitivity (f y); assumption
-      |  (* symmetry *) intros; symmetry  in |- *; assumption ].
+      |  (* symmetry *) intros; symmetry ; assumption ].
 Qed.