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

1 files changed, 30 insertions, 30 deletions

diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v
index 7097159c7..490bf745a 100644
--- a/theories/NArith/Ndist.v
+++ b/theories/NArith/Ndist.v
@@ -33,7 +33,7 @@ Definition Nplength (a:N) :=
 Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0.
 Proof.
   simple induction a; trivial.
-  unfold Nplength in |- *; intros; discriminate H.
+  unfold Nplength; intros; discriminate H.
 Qed.
 
 Lemma Nplength_zeros :
@@ -46,9 +46,9 @@ Proof.
   intros. simpl in H1. discriminate H1.
   simple induction k. trivial.
   generalize H0. case n. intros. inversion H3.
-  intros. simpl in |- *. unfold N.testbit_nat in H. apply (H n0). simpl in H1. inversion H1. reflexivity.
+  intros. simpl. unfold N.testbit_nat in H. apply (H n0). simpl in H1. inversion H1. reflexivity.
   exact (lt_S_n n1 n0 H3).
-  simpl in |- *. intros n H. inversion H. intros. inversion H0.
+  simpl. intros n H. inversion H. intros. inversion H0.
 Qed.
 
 Lemma Nplength_one :
@@ -56,7 +56,7 @@ Lemma Nplength_one :
 Proof.
   simple induction a. intros. inversion H.
   simple induction p. intros. simpl in H0. inversion H0. reflexivity.
-  intros. simpl in H0. inversion H0. simpl in |- *. unfold N.testbit_nat in H. apply H. reflexivity.
+  intros. simpl in H0. inversion H0. simpl. unfold N.testbit_nat in H. apply H. reflexivity.
   intros. simpl in H. inversion H. reflexivity.
 Qed.
 
@@ -70,9 +70,9 @@ Proof.
   intros. absurd (N.testbit_nat (Npos (xI p0)) 0 = false). trivial with bool.
   auto with bool arith.
   intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3.
-  intros. simpl in |- *. unfold Nplength in H.
+  intros. simpl. unfold Nplength in H.
   cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity.
-  apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4.
+  apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false). apply H2. apply lt_n_S. exact H4.
   exact H3.
   intro. case n. trivial.
   intros. simpl in H0. discriminate H0.
@@ -90,10 +90,10 @@ Definition ni_min (d d':natinf) :=
 Lemma ni_min_idemp : forall d:natinf, ni_min d d = d.
 Proof.
   simple induction d; trivial.
-  unfold ni_min in |- *.
+  unfold ni_min.
   simple induction n; trivial.
   intros.
-  simpl in |- *.
+  simpl.
   inversion H.
   rewrite H1.
   rewrite H1.
@@ -105,7 +105,7 @@ Proof.
   simple induction d. simple induction d'; trivial.
   simple induction d'; trivial. elim n. simple induction n0; trivial.
   intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0).
-  intro. unfold ni_min in |- *. simpl in |- *. rewrite H1. reflexivity.
+  intro. unfold ni_min. simpl. rewrite H1. reflexivity.
   cut (ni (min n0 n2) = ni (min n2 n0)). intros.
   inversion H1; trivial.
   exact (H n2).
@@ -116,11 +116,11 @@ Lemma ni_min_assoc :
 Proof.
   simple induction d; trivial. simple induction d'; trivial.
   simple induction d''; trivial.
-  unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)).
+  unfold ni_min. intro. cut (min (min n n0) n1 = min n (min n0 n1)).
   intro. rewrite H. reflexivity.
   generalize n0 n1. elim n; trivial.
   simple induction n3; trivial. simple induction n5; trivial.
-  intros. simpl in |- *. auto.
+  intros. simpl. auto.
 Qed.
 
 Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0.
@@ -152,42 +152,42 @@ Qed.
 
 Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'.
 Proof.
-  unfold ni_le in |- *. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial.
+  unfold ni_le. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial.
 Qed.
 
 Lemma ni_le_trans :
  forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''.
 Proof.
-  unfold ni_le in |- *. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity.
+  unfold ni_le. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity.
 Qed.
 
 Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d.
 Proof.
-  unfold ni_le in |- *. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc.
+  unfold ni_le. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc.
   rewrite ni_min_idemp. reflexivity.
 Qed.
 
 Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'.
 Proof.
-  unfold ni_le in |- *. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity.
+  unfold ni_le. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity.
 Qed.
 
 Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'.
 Proof.
   simple induction d. intro. right. exact (ni_min_inf_l d').
   simple induction d'. left. exact (ni_min_inf_r (ni n)).
-  unfold ni_min in |- *. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0).
+  unfold ni_min. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0).
   intros. case (H n0). intro. left. rewrite H0. reflexivity.
   intro. right. rewrite H0. reflexivity.
   elim n. intro. left. reflexivity.
   simple induction n1. right. reflexivity.
-  intros. case (H n2). intro. left. simpl in |- *. rewrite H1. reflexivity.
-  intro. right. simpl in |- *. rewrite H1. reflexivity.
+  intros. case (H n2). intro. left. simpl. rewrite H1. reflexivity.
+  intro. right. simpl. rewrite H1. reflexivity.
 Qed.
 
 Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d.
 Proof.
-  unfold ni_le in |- *. intros. rewrite (ni_min_comm d' d). apply ni_min_case.
+  unfold ni_le. intros. rewrite (ni_min_comm d' d). apply ni_min_case.
 Qed.
 
 Lemma ni_le_min_induc :
@@ -201,7 +201,7 @@ Proof.
   apply ni_le_antisym. apply H1. apply ni_le_refl.
   exact H2.
   exact H.
-  intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le in |- *. rewrite ni_min_comm. exact H2.
+  intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le. rewrite ni_min_comm. exact H2.
   apply ni_le_refl.
   exact H0.
 Qed.
@@ -209,15 +209,15 @@ Qed.
 Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n).
 Proof.
   cut (forall m n:nat, m <= n -> min m n = m).
-  intros. unfold ni_le, ni_min in |- *. rewrite (H m n H0). reflexivity.
+  intros. unfold ni_le, ni_min. rewrite (H m n H0). reflexivity.
   simple induction m. trivial.
   simple induction n0. intro. inversion H0.
-  intros. simpl in |- *. rewrite (H n1 (le_S_n n n1 H1)). reflexivity.
+  intros. simpl. rewrite (H n1 (le_S_n n n1 H1)). reflexivity.
 Qed.
 
 Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n.
 Proof.
-  unfold ni_le in |- *. unfold ni_min in |- *. intros. inversion H. apply le_min_r.
+  unfold ni_le. unfold ni_min. intros. inversion H. apply le_min_r.
 Qed.
 
 Lemma Nplength_lb :
@@ -225,7 +225,7 @@ Lemma Nplength_lb :
    (forall k:nat, k < n -> N.testbit_nat a k = false) -> ni_le (ni n) (Nplength a).
 Proof.
   simple induction a. intros. exact (ni_min_inf_r (ni n)).
-  intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial.
+  intros. unfold Nplength. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial.
   intro. absurd (N.testbit_nat (Npos p) (Pplength p) = false).
   rewrite
    (Nplength_one (Npos p) (Pplength p)
@@ -238,7 +238,7 @@ Lemma Nplength_ub :
  forall (a:N) (n:nat), N.testbit_nat a n = true -> ni_le (Nplength a) (ni n).
 Proof.
   simple induction a. intros. discriminate H.
-  intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial.
+  intros. unfold Nplength. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial.
   intro. absurd (N.testbit_nat (Npos p) n = true).
   rewrite
    (Nplength_zeros (Npos p) (Pplength p)
@@ -262,7 +262,7 @@ Definition Npdist (a a':N) := Nplength (N.lxor a a').
 
 Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty.
 Proof.
-  intros. unfold Npdist in |- *. rewrite N.lxor_nilpotent. reflexivity.
+  intros. unfold Npdist. rewrite N.lxor_nilpotent. reflexivity.
 Qed.
 
 Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'.
@@ -274,7 +274,7 @@ Qed.
 
 Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a.
 Proof.
-  unfold Npdist in |- *. intros. rewrite N.lxor_comm. reflexivity.
+  unfold Npdist. intros. rewrite N.lxor_comm. reflexivity.
 Qed.
 
 (** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq
@@ -296,8 +296,8 @@ Lemma Nplength_ultra_1 :
 Proof.
   simple induction a. intros. unfold ni_le in H. unfold Nplength at 1 3 in H.
   rewrite (ni_min_inf_l (Nplength a')) in H.
-  rewrite (Nplength_infty a' H). simpl in |- *. apply ni_le_refl.
-  intros. unfold Nplength at 1 in |- *. apply Nplength_lb. intros.
+  rewrite (Nplength_infty a' H). simpl. apply ni_le_refl.
+  intros. unfold Nplength at 1. apply Nplength_lb. intros.
   cut (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false).
   intros. apply H1. reflexivity.
   intro a''. case a''. intro. reflexivity.
@@ -329,7 +329,7 @@ Lemma Npdist_ultra :
  forall a a' a'':N,
    ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a').
 Proof.
-  intros. unfold Npdist in |- *. cut (N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a').
+  intros. unfold Npdist. cut (N.lxor (N.lxor a a'') (N.lxor a'' a') = N.lxor a a').
   intro. rewrite <- H. apply Nplength_ultra.
   rewrite N.lxor_assoc. rewrite <- (N.lxor_assoc a'' a'' a'). rewrite N.lxor_nilpotent.
   rewrite N.lxor_0_l. reflexivity.