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

10 files changed, 44 insertions, 44 deletions

diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index b17adef678..ccce3bbe10 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -9,7 +9,7 @@ Functional Scheme iszero_ind := Induction for iszero Sort Prop.
 
 Lemma toto : forall n : nat, n = 0 -> iszero n = true.
 intros x eg.
- functional induction iszero x; simpl in |- *.
+ functional induction iszero x; simpl.
 trivial.
 inversion eg.
 Qed.
@@ -212,19 +212,19 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
 
 Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
 intros a b.
- functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto.
+ functional induction plus_x_not_five'' a b; intros hyp; simpl; auto.
 Qed.
 
 Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
 intros n m.
- functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
+ functional induction nat_equal_bool n m; simpl; intros hyp; auto.
 rewrite <- hyp in y; simpl in y;tauto.
 inversion hyp.
 Qed.
 
 Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
 intros n m.
- functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto.
+ functional induction nat_equal_bool n m; simpl; intros eg; auto.
 inversion eg.
 inversion eg.
 Qed.
@@ -245,7 +245,7 @@ Qed.
 
 Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
 intros n.
-unfold plus in |- *.
+unfold plus.
  functional induction plus n 0; intros.
 auto with arith.
 apply le_n_S.
@@ -266,7 +266,7 @@ Function mod2 (n : nat) : nat :=
 
 Lemma princ_mod2 : forall n : nat, mod2 n <= n.
 intros n.
- functional induction mod2 n; simpl in |- *; auto with arith.
+ functional induction mod2 n; simpl; auto with arith.
 Qed.
 
 Function isfour (n : nat) : bool :=
@@ -284,7 +284,7 @@ Function isononeorfour (n : nat) : bool :=
 
 Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
 intros n.
- functional induction isononeorfour n; intros istr; simpl in |- *;
+ functional induction isononeorfour n; intros istr; simpl;
  inversion istr.
 apply istrue0.
 destruct n. inversion istr.
@@ -367,7 +367,7 @@ Function ftest2 (n m : nat) {struct n} : nat :=
 
 Lemma test2' : forall n m : nat, ftest2 n m <= 2.
 intros n m.
- functional induction ftest2 n m; simpl in |- *; intros; auto.
+ functional induction ftest2 n m; simpl; intros; auto.
 Qed.
 
 Function ftest3 (n m : nat) {struct n} : nat :=
@@ -387,7 +387,7 @@ auto.
 intros.
 auto.
 intros.
-simpl in |- *.
+simpl.
 auto.
 Qed.
 
@@ -408,7 +408,7 @@ auto.
 intros.
 auto.
 intros.
-simpl in |- *.
+simpl.
 auto.
 Qed.
 
@@ -451,7 +451,7 @@ Qed.
 
 Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
 intros n m.
- functional induction ftest6 n m; simpl in |- *; auto.
+ functional induction ftest6 n m; simpl; auto.
 Qed.
 
 (* Some tests with modules *)
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v
index 89b3032c02..c2d5cb2f47 100644
--- a/test-suite/success/Reg.v
+++ b/test-suite/success/Reg.v
@@ -39,7 +39,7 @@ Lemma essai7 :
  derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1.
 reg.
 apply Rlt_0_1.
-red in |- *; intro;  rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
+red; intro;  rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
  assumption.
 Qed.
 
@@ -127,7 +127,7 @@ Lemma essai23 :
    (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1.
 reg.
 left; apply Rlt_0_1.
-right; unfold Rminus in |- *;  rewrite Rplus_opp_r; reflexivity.
+right; unfold Rminus;  rewrite Rplus_opp_r; reflexivity.
 Qed.
 
 Lemma essai24 :
@@ -135,8 +135,8 @@ Lemma essai24 :
 reg.
  replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R.
 apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ].
-unfold Rsqr in |- *;  ring.
-red in |- *; intro; cut (0 < x * x + 1)%R.
+unfold Rsqr;  ring.
+red; intro; cut (0 < x * x + 1)%R.
 intro;  rewrite H in H0; elim (Rlt_irrefl _ H0).
 apply Rplus_le_lt_0_compat;
  [  replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ]
diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v
index b356f277c3..361c787e25 100644
--- a/test-suite/success/Try.v
+++ b/test-suite/success/Try.v
@@ -2,7 +2,7 @@
    non-existent names in Unfold [cf bug #263] *)
 
 Lemma lem1 : True.
-try unfold i_dont_exist in |- *.
+try unfold i_dont_exist.
 trivial.
 Qed.
 
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index c65cf3036c..7bed7ecb15 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -14,7 +14,7 @@ Abort.
 (* Check the combination of at, with and in (see bug #2146) *)
 
 Goal 3=3 -> 3=3. intro H.
-change 3 at 2 with (1+2) in |- *.
+change 3 at 2 with (1+2).
 change 3 at 2 with (1+2) in H |-.
 change 3 with (1+2) in H at 1 |- * at 1.
 (* Now check that there are no more 3's *)
@@ -25,10 +25,10 @@ Qed.
 change 3 at 1 with (1+2) at 3.
 change 3 at 1 with (1+2) in *.
 change 3 at 1 with (1+2) in H at 2 |-.
-change 3 at 1 with (1+2) in |- * at 3.
+change 3 at 1 with (1+2) at 3.
 change 3 at 1 with (1+2) in H |- *.
 change 3 at 1 with (1+2) in H, H|-.
-change 3 in |- * at 1.
+change 3 at 1.
  *)
 
 (* Test that pretyping checks allowed elimination sorts *)
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 23e3caf8a3..8623f71868 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -16,9 +16,9 @@ intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
  generalize (nat_of_P_gt_Gt_compare_morphism n m);
  generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont n m Eq).
 intros H' H'0 H'1; right; right; auto.
-intros H' H'0 H'1; left; unfold rlt in |- *.
+intros H' H'0 H'1; left; unfold rlt.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
-intros H' H'0 H'1; right; left; unfold rlt in |- *.
+intros H' H'0 H'1; right; left; unfold rlt.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
 apply H'0; auto.
 Defined.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 01ebfc4f04..8ed941f864 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -46,21 +46,21 @@ Qed.
 
 Goal forall x, S x = S (S x).   
 intros.
-induction (S _) in |- * at -2.
+induction (S _) at -2.
 now_show (0=1).
 Undo 2.
-induction (S _) in |- * at 1 3.
+induction (S _) at 1 3.
 now_show (0=1).
 Undo 2.
-induction (S _) in |- * at 1.
+induction (S _) at 1.
 now_show (0=S (S x)).
 Undo 2.
-induction (S _) in |- * at 2.
+induction (S _) at 2.
 now_show (S x=0).
 Undo 2.
-induction (S _) in |- * at 3.
+induction (S _) at 3.
 now_show (S x=1).
 Undo 2.
-Fail induction (S _) in |- * at 4.
+Fail induction (S _) at 4.
 Abort.
 
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 0c8a181673..1edddcfd74 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -2,7 +2,7 @@
 
 (* Submitted by Pierre Crégut *)
 (* Checks substitution of x *)
-Ltac f x := unfold x in |- *; idtac.
+Ltac f x := unfold x; idtac.
 
 Lemma lem1 : 0 + 0 = 0.
 f plus.
@@ -86,7 +86,7 @@ assert t.
 exact H.
 intro H1.
 apply H.
-symmetry  in |- *.
+symmetry .
 assumption.
 Qed.
 
@@ -105,7 +105,7 @@ sym'.
 exact H.
 intro H1.
 apply H.
-symmetry  in |- *.
+symmetry .
 assumption.
 Qed.
 
@@ -193,7 +193,7 @@ Abort.
 (* Used to fail in V8.1 *)
 
 Tactic Notation "test" constr(t) integer(n) :=
-   set (k := t) in |- * at n.
+   set (k := t) at n.
 
 Goal forall x : nat, x = 1 -> x + x + x = 3.
 intros x H.
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 3241e1339b..5f8ed03d3f 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -4,5 +4,5 @@ Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
 intros.
 Fail remember nat as X.
 Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
-Fail remember nat as X in |- *.
+Fail remember nat as X.
 Abort.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 19693d70c9..653b5bf9a5 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -18,10 +18,10 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
 
 Lemma setoid_set : Setoid_Theory set same.
 
-unfold same in |- *; split ; red.
-red in |- *; auto.
+unfold same; split ; red.
+red; auto.
 
-red in |- *.
+red.
 intros.
 elim (H a); auto.
 
@@ -33,19 +33,19 @@ Qed.
 Add Setoid set same setoid_set as setsetoid.
 
 Add Morphism In : In_ext.
-unfold same in |- *; intros a s t H; elim (H a); auto.
+unfold same; intros a s t H; elim (H a); auto.
 Qed.
 
 Lemma add_aux :
  forall s t : set,
  same s t -> forall a b : A, In a (Add b s) -> In a (Add b t).
-unfold same in |- *; simple induction 2; intros.
+unfold same; simple induction 2; intros.
 rewrite H1.
-simpl in |- *; left; reflexivity.
+simpl; left; reflexivity.
 
 elim (H a).
 intros.
-simpl in |- *; right.
+simpl; right.
 apply (H2 H1).
 Qed.
 
@@ -74,15 +74,15 @@ setoid_replace (remove a (Add a Empty)) with Empty.
 
 auto.
 
-unfold same in |- *.
+unfold same.
 split.
-simpl in |- *.
+simpl.
 case (eq_dec a a).
 intros e ff; elim ff.
 
 intros; absurd (a = a); trivial.
 
-simpl in |- *.
+simpl.
 intro H; elim H.
 Qed.
 
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 469cbeb74d..e00701fb68 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -16,7 +16,7 @@ auto.
 Qed.
 
 Lemma lem3 : forall P : Prop, P.
-intro P; pattern P in |- *.
+intro P; pattern P.
 apply lem2.
 Abort.
 
@@ -34,7 +34,7 @@ Require Import Relations.
 
 Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X).
 Proof.
-  unfold transitive in |- *.
+  unfold transitive.
   intros X f g h H1 H2.
   inversion H1.
 Abort.