From ffb64d16132dd80f72ecb619ef87e3eee1fa8bda Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 5 Jul 2012 16:56:37 +0000
Subject: Kills the useless tactic annotations "in |- *"

 Most of these heavyweight annotations were introduced a long time ago
 by the automatic 7.x -> 8.0 translator

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Relations/Operators_Properties.v | 6 +++---
 theories/Relations/Relations.v            | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

(limited to 'theories/Relations')

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index f7f5512e7..3f3810083 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -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/Relations.v b/theories/Relations/Relations.v
index f9fb2c442..ed2567396 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -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.
 
-- 
cgit v1.2.3