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

6 files changed, 46 insertions, 46 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 8d535d509..06c9988a1 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -151,7 +151,7 @@ Proof.
   intro.
   apply False_rec.
   apply H.
-  symmetry  in |- *.
+  symmetry .
   assumption.
 Defined.
 
@@ -174,7 +174,7 @@ Proof.
   assumption.
   intro.
   right.
-  symmetry  in |- *.
+  symmetry .
   assumption.
 Defined.
 
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 7ae2a67ca..02e3ffe47 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -56,7 +56,7 @@ Proof.
   set (Q := fun z => 0 <= z -> P z * P (- z)) in *.
   cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ].
   elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
-  unfold Q in |- *; clear Q; intros.
+  unfold Q; clear Q; intros.
   split; apply HP.
   rewrite Z.abs_eq; auto; intros.
   elim (H (Z.abs m)); intros; auto with zarith.
@@ -75,7 +75,7 @@ Proof.
   set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.
   cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ].
   elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
-  unfold Q in |- *; clear Q; intros.
+  unfold Q; clear Q; intros.
   split; apply HP.
   rewrite Z.abs_eq; auto; intros.
   elim (H (Z.abs m)); intros; auto with zarith.
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index a9348785a..d252b3e92 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -90,13 +90,13 @@ Section ENCODING_VALUE.
   Lemma Zmod2_twice :
     forall z:Z, z = (2 * Zmod2 z + bit_value (Z.odd z))%Z.
   Proof.
-    destruct z; simpl in |- *.
+    destruct z; simpl.
     trivial.
 
-    destruct p; simpl in |- *; trivial.
+    destruct p; simpl; trivial.
 
-    destruct p; simpl in |- *.
-    destruct p as [p| p| ]; simpl in |- *.
+    destruct p; simpl.
+    destruct p as [p| p| ]; simpl.
     rewrite <- (Pos.pred_double_succ p); trivial.
 
     trivial.
@@ -145,17 +145,17 @@ Section Z_BRIC_A_BRAC.
       (z >= 0)%Z ->
       Z_to_binary (S n) (bit_value b + 2 * z) = Bcons b n (Z_to_binary n z).
   Proof.
-    destruct b; destruct z; simpl in |- *; auto.
+    destruct b; destruct z; simpl; auto.
     intro H; elim H; trivial.
   Qed.
 
   Lemma binary_value_pos :
     forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z.
   Proof.
-    induction bv as [| a n v IHbv]; simpl in |- *.
+    induction bv as [| a n v IHbv]; simpl.
     omega.
 
-    destruct a; destruct (binary_value n v); simpl in |- *; auto.
+    destruct a; destruct (binary_value n v); simpl; auto.
     auto with zarith.
   Qed.
 
@@ -174,7 +174,7 @@ Section Z_BRIC_A_BRAC.
   Proof.
     destruct b; destruct z as [| p| p]; auto.
     destruct p as [p| p| ]; auto.
-    destruct p as [p| p| ]; simpl in |- *; auto.
+    destruct p as [p| p| ]; simpl; auto.
     intros; rewrite (Pos.succ_pred_double p); trivial.
   Qed.
 
@@ -201,7 +201,7 @@ Section Z_BRIC_A_BRAC.
     auto.
 
     destruct p; auto.
-    simpl in |- *; intros; omega.
+    simpl; intros; omega.
 
     intro H; elim H; trivial.
   Qed.
@@ -233,7 +233,7 @@ Section Z_BRIC_A_BRAC.
   Lemma Zeven_bit_value :
     forall z:Z, Zeven.Zeven z -> bit_value (Z.odd z) = 0%Z.
   Proof.
-    destruct z; unfold bit_value in |- *; auto.
+    destruct z; unfold bit_value; auto.
     destruct p; tauto || (intro H; elim H).
     destruct p; tauto || (intro H; elim H).
   Qed.
@@ -241,7 +241,7 @@ Section Z_BRIC_A_BRAC.
   Lemma Zodd_bit_value :
     forall z:Z, Zeven.Zodd z -> bit_value (Z.odd z) = 1%Z.
   Proof.
-    destruct z; unfold bit_value in |- *; auto.
+    destruct z; unfold bit_value; auto.
     intros; elim H.
     destruct p; tauto || (intros; elim H).
     destruct p; tauto || (intros; elim H).
@@ -310,7 +310,7 @@ Section COHERENT_VALUE.
       (z < two_power_nat n)%Z -> binary_value n (Z_to_binary n z) = z.
   Proof.
     induction n as [| n IHn].
-    unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros; omega.
+    unfold two_power_nat, shift_nat; simpl; intros; omega.
 
     intros; rewrite Z_to_binary_Sn_z.
     rewrite binary_value_Sn.
@@ -328,7 +328,7 @@ Section COHERENT_VALUE.
       (z < two_power_nat n)%Z -> two_compl_value n (Z_to_two_compl n z) = z.
   Proof.
     induction n as [| n IHn].
-    unfold two_power_nat, shift_nat in |- *; simpl in |- *; intros.
+    unfold two_power_nat, shift_nat; simpl; intros.
     assert (z = (-1)%Z \/ z = 0%Z). omega.
     intuition; subst z; trivial.
 
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 3711ea021..09323ebd4 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -77,7 +77,7 @@ Section Log_pos. (* Log of positive integers *)
     forall x:positive,
       0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Z.succ (log_inf x)).
   Proof.
-    simple induction x; intros; simpl in |- *;
+    simple induction x; intros; simpl;
       [ elim H; intros Hp HR; clear H; split;
 	[ auto with zarith
 	  | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial);
@@ -90,7 +90,7 @@ Section Log_pos. (* Log of positive integers *)
 	      rewrite two_p_S by trivial;
 	      rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xO p);
 		  omega ]
-	| unfold two_power_pos in |- *; unfold shift_pos in |- *; simpl in |- *;
+	| unfold two_power_pos; unfold shift_pos; simpl;
 	  omega ].
   Qed.
 
@@ -103,7 +103,7 @@ Section Log_pos. (* Log of positive integers *)
 
   Lemma log_sup_correct1 : forall p:positive, 0 <= log_sup p.
   Proof.
-    simple induction p; intros; simpl in |- *; auto with zarith.
+    simple induction p; intros; simpl; auto with zarith.
   Qed.
 
   (** For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)]
@@ -115,16 +115,16 @@ Section Log_pos. (* Log of positive integers *)
     else log_sup p = Z.succ (log_inf p).
   Proof.
     simple induction p; intros;
-      [ elim H; right; simpl in |- *;
+      [ elim H; right; simpl;
 	rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
 	  rewrite BinInt.Pos2Z.inj_xI; unfold Z.succ; omega
 	| elim H; clear H; intro Hif;
-	  [ left; simpl in |- *;
+	  [ left; simpl;
 	    rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
 	      rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0));
 		rewrite <- (proj1 Hif); rewrite <- (proj2 Hif);
 		  auto
-	    | right; simpl in |- *;
+	    | right; simpl;
 	      rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
 		rewrite BinInt.Pos2Z.inj_xO; unfold Z.succ;
 		  omega ]
@@ -146,12 +146,12 @@ Section Log_pos. (* Log of positive integers *)
 
   Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p.
   Proof.
-    simple induction p; simpl in |- *; intros; omega.
+    simple induction p; simpl; intros; omega.
   Qed.
 
   Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Z.succ (log_inf p).
   Proof.
-    simple induction p; simpl in |- *; intros; omega.
+    simple induction p; simpl; intros; omega.
   Qed.
 
   (** Now it's possible to specify and build the [Log] rounded to the nearest *)
@@ -167,7 +167,7 @@ Section Log_pos. (* Log of positive integers *)
 
   Theorem log_near_correct1 : forall p:positive, 0 <= log_near p.
   Proof.
-    simple induction p; simpl in |- *; intros;
+    simple induction p; simpl; intros;
       [ elim p0; auto with zarith
 	| elim p0; auto with zarith
 	| trivial with zarith ].
@@ -182,9 +182,9 @@ Section Log_pos. (* Log of positive integers *)
   Proof.
     simple induction p.
     intros p0 [Einf| Esup].
-    simpl in |- *. rewrite Einf.
+    simpl. rewrite Einf.
     case p0; [ left | left | right ]; reflexivity.
-    simpl in |- *; rewrite Esup.
+    simpl; rewrite Esup.
     elim (log_sup_log_inf p0).
     generalize (log_inf_le_log_sup p0).
     generalize (log_sup_le_Slog_inf p0).
@@ -192,10 +192,10 @@ Section Log_pos. (* Log of positive integers *)
     intros; omega.
     case p0; intros; auto with zarith.
     intros p0 [Einf| Esup].
-    simpl in |- *.
+    simpl.
     repeat rewrite Einf.
     case p0; intros; auto with zarith.
-    simpl in |- *.
+    simpl.
     repeat rewrite Esup.
     case p0; intros; auto with zarith.
     auto.
@@ -216,7 +216,7 @@ Section divers.
 
   Lemma ZERO_le_N_digits : forall x:Z, 0 <= N_digits x.
   Proof.
-    simple induction x; simpl in |- *;
+    simple induction x; simpl;
       [ apply Z.le_refl | exact log_inf_correct1 | exact log_inf_correct1 ].
   Qed.
 
@@ -245,21 +245,21 @@ Section divers.
   Proof.
     split;
       [ elim p;
-	[ simpl in |- *; tauto
-	  | simpl in |- *; intros; generalize (H H0); intro H1; elim H1;
+	[ simpl; tauto
+	  | simpl; intros; generalize (H H0); intro H1; elim H1;
 	    intros y0 Hy0; exists (S y0); rewrite Hy0; reflexivity
 	  | intro; exists 0%nat; reflexivity ]
-	| intros; elim H; intros; rewrite H0; elim x; intros; simpl in |- *; trivial ].
+	| intros; elim H; intros; rewrite H0; elim x; intros; simpl; trivial ].
   Qed.
 
   Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p.
   Proof.
     simple induction p;
-      [ intros; right; simpl in |- *; tauto
+      [ intros; right; simpl; tauto
 	| intros; elim H;
-	  [ intros; left; simpl in |- *; exact H0
-	    | intros; right; simpl in |- *; exact H0 ]
-	| left; simpl in |- *; trivial ].
+	  [ intros; left; simpl; exact H0
+	    | intros; right; simpl; exact H0 ]
+	| left; simpl; trivial ].
   Qed.
 
 End divers.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 33f4dc7f4..5d6550f99 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -305,7 +305,7 @@ Section extended_euclid_algorithm.
 	v1 * a + v2 * b = v3 ->
 	(forall d:Z, Zis_gcd u3 v3 d -> Zis_gcd a b d) -> Euclid.
   Proof.
-    intros v3 Hv3; generalize Hv3; pattern v3 in |- *.
+    intros v3 Hv3; generalize Hv3; pattern v3.
     apply Zlt_0_rec.
     clear v3 Hv3; intros.
     elim (Z_zerop x); intro.
@@ -319,8 +319,8 @@ Section extended_euclid_algorithm.
     apply Z_mod_lt; omega.
     assert (xpos : x > 0). omega.
     generalize (Z_div_mod_eq u3 x xpos).
-    unfold q in |- *.
-    intro eq; pattern u3 at 2 in |- *; rewrite eq; ring.
+    unfold q.
+    intro eq; pattern u3 at 2; rewrite eq; ring.
     apply (H (u3 - q * x) Hq (proj1 Hq) v1 v2 x (u1 - q * v1) (u2 - q * v2)).
     tauto.
     replace ((u1 - q * v1) * a + (u2 - q * v2) * b) with
@@ -459,12 +459,12 @@ Proof.
   apply Gauss with a.
   rewrite H3.
   auto with zarith.
-  red in |- *; auto with zarith.
+  red; auto with zarith.
   apply Gauss with c.
   rewrite Z.mul_comm.
   rewrite <- H3.
   auto with zarith.
-  red in |- *; auto with zarith.
+  red; auto with zarith.
 Qed.
 
 (** After factorization by a gcd, the original numbers are relatively prime. *)
@@ -479,7 +479,7 @@ Proof.
   elim H1; intros.
   elim H4; intros.
   rewrite H2 in H6; subst b; omega.
-  unfold rel_prime in |- *.
+  unfold rel_prime.
   destruct H1.
   destruct H1 as (a',H1).
   destruct H3 as (b',H3).
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 0a4418671..6f005d01d 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -32,13 +32,13 @@ Section wf_proof.
   Let f (z:Z) := Z.abs_nat (z - c).
 
   Lemma Zwf_well_founded : well_founded (Zwf c).
-    red in |- *; intros.
+    red; intros.
     assert (forall (n:nat) (a:Z), (f a < n)%nat \/ a < c -> Acc (Zwf c) a).
     clear a; simple induction n; intros.
   (** n= 0 *)
     case H; intros.
     case (lt_n_O (f a)); auto.
-    apply Acc_intro; unfold Zwf in |- *; intros.
+    apply Acc_intro; unfold Zwf; intros.
     assert False; omega || contradiction.
   (** inductive case *)
     case H0; clear H0; intro; auto.