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

8 files changed, 33 insertions, 33 deletions

diff --git a/theories/Logic/Berardi.v b/theories/Logic/Berardi.v
index 2b3886874..58e339b4c 100644
--- a/theories/Logic/Berardi.v
+++ b/theories/Logic/Berardi.v
@@ -45,7 +45,7 @@ Lemma AC_IF :
    (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
 Proof.
 intros P B e1 e2 Q p1 p2.
-unfold IFProp in |- *.
+unfold IFProp.
 case (EM B); assumption.
 Qed.
 
@@ -76,7 +76,7 @@ Record retract_cond : Prop :=
 Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
 Proof.
 intros r.
-case r; simpl in |- *.
+case r; simpl.
 trivial.
 Qed.
 
@@ -113,7 +113,7 @@ Lemma retract_pow_U_U : retract (pow U) U.
 Proof.
 exists g f.
 intro a.
-unfold f, g in |- *; simpl in |- *.
+unfold f, g; simpl.
 apply AC.
 exists (fun x:pow U => x) (fun x:pow U => x).
 trivial.
@@ -130,8 +130,8 @@ Definition R : U := g (fun u:U => Not_b (u U u)).
 
 Lemma not_has_fixpoint : R R = Not_b (R R).
 Proof.
-unfold R at 1 in |- *.
-unfold g in |- *.
+unfold R at 1.
+unfold g.
 rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
 trivial.
 exists (fun x:pow U => x) (fun x:pow U => x); trivial.
@@ -141,7 +141,7 @@ Qed.
 Theorem classical_proof_irrelevence : T = F.
 Proof.
 generalize not_has_fixpoint.
-unfold Not_b in |- *.
+unfold Not_b.
 apply AC_IF.
 intros is_true is_false.
 elim is_true; elim is_false; trivial.
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 8b11f09b9..b93b7688a 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -345,7 +345,7 @@ Lemma rel_choice_and_proof_irrel_imp_guarded_rel_choice :
   RelationalChoice -> ProofIrrelevance -> GuardedRelationalChoice.
 Proof.
   intros rel_choice proof_irrel.
-  red in |- *; intros A B P R H.
+  red; intros A B P R H.
   destruct (rel_choice _ _ (fun (x:sigT P) (y:B) => R (projT1 x) y)) as (R',(HR'R,H0)).
   intros (x,HPx).
   destruct (H x HPx) as (y,HRxy).
@@ -581,7 +581,7 @@ Lemma classical_denumerable_description_imp_fun_choice :
       (forall x y, decidable (R x y)) -> FunctionalChoice_on_rel R.
 Proof.
   intros A Descr.
-  red in |- *; intros R Rdec H.
+  red; intros R Rdec H.
   set (R':= fun x y => R x y /\ forall y', R x y' -> y <= y').
   destruct (Descr R') as (f,Hf).
   intro x.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 2e1e99e8a..07ed643b7 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -148,7 +148,7 @@ Proof.
   case (prop_ext_retract_A_A_imp_A Ext A a); intros g1 g2 g1_o_g2.
   exists (fun f => (fun x:A => f (g1 x x)) (g2 (fun x => f (g1 x x)))).
   intro f.
-  pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1 in |- *.
+  pattern (g1 (g2 (fun x:A => f (g1 x x)))) at 1.
   rewrite (g1_o_g2 (fun x:A => f (g1 x x))).
   reflexivity.
 Qed.
@@ -192,12 +192,12 @@ Section Proof_irrelevance_gen.
     case (ext_prop_fixpoint Ext bool true); intros G Gfix.
     set (neg := fun b:bool => bool_elim bool false true b).
     generalize (eq_refl (G neg)).
-    pattern (G neg) at 1 in |- *.
+    pattern (G neg) at 1.
     apply Ind with (b := G neg); intro Heq.
     rewrite (bool_elim_redl bool false true).
-    change (true = neg true) in |- *; rewrite Heq; apply Gfix.
+    change (true = neg true); rewrite Heq; apply Gfix.
     rewrite (bool_elim_redr bool false true).
-    change (neg false = false) in |- *; rewrite Heq; symmetry  in |- *;
+    change (neg false = false); rewrite Heq; symmetry ;
       apply Gfix.
   Qed.
 
@@ -207,9 +207,9 @@ Section Proof_irrelevance_gen.
     intros Ext Ind A a1 a2.
     set (f := fun b:bool => bool_elim A a1 a2 b).
     rewrite (bool_elim_redl A a1 a2).
-    change (f true = a2) in |- *.
+    change (f true = a2).
     rewrite (bool_elim_redr A a1 a2).
-    change (f true = f false) in |- *.
+    change (f true = f false).
     rewrite (aux Ext Ind).
     reflexivity.
   Qed.
@@ -344,8 +344,8 @@ Section Proof_irrelevance_EM_CC.
 
   Lemma p2p1 : forall A:Prop, A -> b2p (p2b A).
   Proof.
-    unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
-      unfold b2p in |- *; intros.
+    unfold p2b; intro A; apply or_dep_elim with (b := em A);
+      unfold b2p; intros.
     apply (or_elim_redl A (~ A) B (fun _ => b1) (fun _ => b2)).
     destruct (b H).
   Qed.
@@ -353,8 +353,8 @@ Section Proof_irrelevance_EM_CC.
   Lemma p2p2 : b1 <> b2 -> forall A:Prop, b2p (p2b A) -> A.
   Proof.
     intro not_eq_b1_b2.
-    unfold p2b in |- *; intro A; apply or_dep_elim with (b := em A);
-      unfold b2p in |- *; intros.
+    unfold p2b; intro A; apply or_dep_elim with (b := em A);
+      unfold b2p; intros.
     assumption.
     destruct not_eq_b1_b2.
     rewrite <- (or_elim_redr A (~ A) B (fun _ => b1) (fun _ => b2)) in H.
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 9d57fe88b..8da364a38 100644
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -42,7 +42,7 @@ Qed.
 Lemma not_ex_all_not :
  forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
 Proof. (* Intuitionistic *)
-unfold not in |- *; intros P notex n abs.
+unfold not; intros P notex n abs.
 apply notex.
 exists n; trivial.
 Qed.
@@ -52,20 +52,20 @@ Lemma not_ex_not_all :
 Proof.
 intros P H n.
 apply NNPP.
-red in |- *; intro K; apply H; exists n; trivial.
+red; intro K; apply H; exists n; trivial.
 Qed.
 
 Lemma ex_not_not_all :
  forall P:U -> Prop, (exists n : U, ~ P n) -> ~ (forall n:U, P n).
 Proof. (* Intuitionistic *)
-unfold not in |- *; intros P exnot allP.
+unfold not; intros P exnot allP.
 elim exnot; auto.
 Qed.
 
 Lemma all_not_not_ex :
  forall P:U -> Prop, (forall n:U, ~ P n) -> ~ (exists n : U, P n).
 Proof. (* Intuitionistic *)
-unfold not in |- *; intros P allnot exP; elim exP; intros n p.
+unfold not; intros P allnot exP; elim exP; intros n p.
 apply allnot with n; auto.
 Qed.
 
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index 5d7764e7e..c48165c61 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -20,7 +20,7 @@ Axiom classic : forall P:Prop, P \/ ~ P.
 
 Lemma NNPP : forall p:Prop, ~ ~ p -> p.
 Proof.
-unfold not in |- *; intros; elim (classic p); auto.
+unfold not; intros; elim (classic p); auto.
 intro NP; elim (H NP).
 Qed.
 
@@ -35,7 +35,7 @@ Qed.
 
 Lemma not_imply_elim : forall P Q:Prop, ~ (P -> Q) -> P.
 Proof.
-intros; apply NNPP; red in |- *.
+intros; apply NNPP; red.
 intro; apply H; intro; absurd P; trivial.
 Qed.
 
@@ -68,7 +68,7 @@ Qed.
 
 Lemma or_not_and : forall P Q:Prop, ~ P \/ ~ Q -> ~ (P /\ Q).
 Proof.
-simple induction 1; red in |- *; simple induction 2; auto.
+simple induction 1; red; simple induction 2; auto.
 Qed.
 
 Lemma not_or_and : forall P Q:Prop, ~ (P \/ Q) -> ~ P /\ ~ Q.
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v
index e8e8b94ce..b5e7b2c41 100644
--- a/theories/Logic/Diaconescu.v
+++ b/theories/Logic/Diaconescu.v
@@ -61,7 +61,7 @@ Variable pred_extensionality : PredicateExtensionality.
 Lemma prop_ext : forall A B:Prop, (A <-> B) -> A = B.
 Proof.
   intros A B H.
-  change ((fun _ => A) true = (fun _ => B) true) in |- *.
+  change ((fun _ => A) true = (fun _ => B) true).
   rewrite
    pred_extensionality with (P := fun _:bool => A) (Q := fun _:bool => B).
     reflexivity.
@@ -134,8 +134,8 @@ right.
 intro HP.
 assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b).
 intro b; split.
-unfold class_of_false in |- *; right; assumption.
-unfold class_of_true in |- *; right; assumption.
+unfold class_of_false; right; assumption.
+unfold class_of_true; right; assumption.
 assert (Heq : class_of_true = class_of_false).
 apply pred_extensionality with (1 := Hequiv).
 apply diff_true_false.
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 2ed5d428c..ba43600fc 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -61,7 +61,7 @@ Section EqdepDec.
 
   Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.
     intros.
-    unfold nu in |- *.
+    unfold nu.
     case (eq_dec x y); intros.
     reflexivity.
 
@@ -75,7 +75,7 @@ Section EqdepDec.
   Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.
   Proof.
     intros.
-    case u; unfold nu_inv in |- *.
+    case u; unfold nu_inv.
     apply trans_sym_eq.
   Qed.
 
@@ -115,7 +115,7 @@ Section EqdepDec.
   Proof.
     intros.
     cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).
-    simpl in |- *.
+    simpl.
     case (eq_dec x x).
     intro e.
     elim e using K_dec; trivial.
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index bb03c6664..cf2c8a16b 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -46,7 +46,7 @@ Lemma Omega : forall i:U -> bool, induct i -> b2p (i WF).
 Proof.
 intros i y.
 apply y.
-unfold le, WF, induct in |- *.
+unfold le, WF, induct.
 apply p2p2.
 intros x H0.
 apply y.
@@ -55,7 +55,7 @@ Qed.
 
 Lemma lemma1 : induct (fun u => p2b (I u)).
 Proof.
-unfold induct in |- *.
+unfold induct.
 intros x p.
 apply (p2p2 (I x)).
 intro q.