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, 63 insertions, 63 deletions

diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 289ffab31..1e824e2ea 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -72,14 +72,14 @@ Fixpoint get (n : nat) (s : string) {struct s} : option ascii :=
 Theorem get_correct :
   forall s1 s2 : string, (forall n : nat, get n s1 = get n s2) <-> s1 = s2.
 Proof.
-intros s1; elim s1; simpl in |- *.
-intros s2; case s2; simpl in |- *; split; auto.
+intros s1; elim s1; simpl.
+intros s2; case s2; simpl; split; auto.
 intros H; generalize (H 0); intros H1; inversion H1.
 intros; discriminate.
-intros a s1' Rec s2; case s2; simpl in |- *; split; auto.
+intros a s1' Rec s2; case s2; simpl; split; auto.
 intros H; generalize (H 0); intros H1; inversion H1.
 intros; discriminate.
-intros H; generalize (H 0); simpl in |- *; intros H1; inversion H1.
+intros H; generalize (H 0); simpl; intros H1; inversion H1.
 case (Rec s).
 intros H0; rewrite H0; auto.
 intros n; exact (H (S n)).
@@ -94,9 +94,9 @@ Theorem append_correct1 :
  forall (s1 s2 : string) (n : nat),
  n < length s1 -> get n s1 = get n (s1 ++ s2).
 Proof.
-intros s1; elim s1; simpl in |- *; auto.
+intros s1; elim s1; simpl; auto.
 intros s2 n H; inversion H.
-intros a s1' Rec s2 n; case n; simpl in |- *; auto.
+intros a s1' Rec s2 n; case n; simpl; auto.
 intros n0 H; apply Rec; auto.
 apply lt_S_n; auto.
 Qed.
@@ -107,10 +107,10 @@ Theorem append_correct2 :
  forall (s1 s2 : string) (n : nat),
  get n s2 = get (n + length s1) (s1 ++ s2).
 Proof.
-intros s1; elim s1; simpl in |- *; auto.
-intros s2 n; rewrite plus_comm; simpl in |- *; auto.
-intros a s1' Rec s2 n; case n; simpl in |- *; auto.
-generalize (Rec s2 0); simpl in |- *; auto. intros.
+intros s1; elim s1; simpl; auto.
+intros s2 n; rewrite plus_comm; simpl; auto.
+intros a s1' Rec s2 n; case n; simpl; auto.
+generalize (Rec s2 0); simpl; auto. intros.
 rewrite <- Plus.plus_Snm_nSm; auto.
 Qed.
 
@@ -135,16 +135,16 @@ Theorem substring_correct1 :
  forall (s : string) (n m p : nat),
  p < m -> get p (substring n m s) = get (p + n) s.
 Proof.
-intros s; elim s; simpl in |- *; auto.
-intros n; case n; simpl in |- *; auto.
-intros m; case m; simpl in |- *; auto.
-intros a s' Rec; intros n; case n; simpl in |- *; auto.
-intros m; case m; simpl in |- *; auto.
+intros s; elim s; simpl; auto.
+intros n; case n; simpl; auto.
+intros m; case m; simpl; auto.
+intros a s' Rec; intros n; case n; simpl; auto.
+intros m; case m; simpl; auto.
 intros p H; inversion H.
-intros m' p; case p; simpl in |- *; auto.
-intros n0 H; apply Rec; simpl in |- *; auto.
+intros m' p; case p; simpl; auto.
+intros n0 H; apply Rec; simpl; auto.
 apply Lt.lt_S_n; auto.
-intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl in |- *; auto.
+intros n' m p H; rewrite <- Plus.plus_Snm_nSm; simpl; auto.
 Qed.
 
 (** The substring has at most [m] elements *)
@@ -152,14 +152,14 @@ Qed.
 Theorem substring_correct2 :
  forall (s : string) (n m p : nat), m <= p -> get p (substring n m s) = None.
 Proof.
-intros s; elim s; simpl in |- *; auto.
-intros n; case n; simpl in |- *; auto.
-intros m; case m; simpl in |- *; auto.
-intros a s' Rec; intros n; case n; simpl in |- *; auto.
-intros m; case m; simpl in |- *; auto.
-intros m' p; case p; simpl in |- *; auto.
+intros s; elim s; simpl; auto.
+intros n; case n; simpl; auto.
+intros m; case m; simpl; auto.
+intros a s' Rec; intros n; case n; simpl; auto.
+intros m; case m; simpl; auto.
+intros m' p; case p; simpl; auto.
 intros H; inversion H.
-intros n0 H; apply Rec; simpl in |- *; auto.
+intros n0 H; apply Rec; simpl; auto.
 apply Le.le_S_n; auto.
 Qed.
 
@@ -188,11 +188,11 @@ Theorem prefix_correct :
  forall s1 s2 : string,
  prefix s1 s2 = true <-> substring 0 (length s1) s2 = s1.
 Proof.
-intros s1; elim s1; simpl in |- *; auto.
-intros s2; case s2; simpl in |- *; split; auto.
-intros a s1' Rec s2; case s2; simpl in |- *; auto.
+intros s1; elim s1; simpl; auto.
+intros s2; case s2; simpl; split; auto.
+intros a s1' Rec s2; case s2; simpl; auto.
 split; intros; discriminate.
-intros b s2'; case (ascii_dec a b); simpl in |- *; auto.
+intros b s2'; case (ascii_dec a b); simpl; auto.
 intros e; case (Rec s2'); intros H1 H2; split; intros H3; auto.
 rewrite e; rewrite H1; auto.
 apply H2; injection H3; auto.
@@ -234,25 +234,25 @@ Theorem index_correct1 :
  forall (n m : nat) (s1 s2 : string),
  index n s1 s2 = Some m -> substring m (length s1) s2 = s1.
 Proof.
-intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl in |- *;
+intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
  auto.
-intros n; case n; simpl in |- *; auto.
-intros m s1; case s1; simpl in |- *; auto.
+intros n; case n; simpl; auto.
+intros m s1; case s1; simpl; auto.
 intros H; injection H; intros H1; rewrite <- H1; auto.
 intros; discriminate.
 intros; discriminate.
 intros b s2' Rec n m s1.
-case n; simpl in |- *; auto.
+case n; simpl; auto.
 generalize (prefix_correct s1 (String b s2'));
  case (prefix s1 (String b s2')).
 intros H0 H; injection H; intros H1; rewrite <- H1; auto.
-case H0; simpl in |- *; auto.
-case m; simpl in |- *; auto.
+case H0; simpl; auto.
+case m; simpl; auto.
 case (index 0 s1 s2'); intros; discriminate.
 intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
 intros x H H0 H1; apply H; injection H1; auto.
 intros; discriminate.
-intros n'; case m; simpl in |- *; auto.
+intros n'; case m; simpl; auto.
 case (index n' s1 s2'); intros; discriminate.
 intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.
 intros x H H1; apply H; injection H1; auto.
@@ -267,35 +267,35 @@ Theorem index_correct2 :
  index n s1 s2 = Some m ->
  forall p : nat, n <= p -> p < m -> substring p (length s1) s2 <> s1.
 Proof.
-intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl in |- *;
+intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
  auto.
-intros n; case n; simpl in |- *; auto.
-intros m s1; case s1; simpl in |- *; auto.
+intros n; case n; simpl; auto.
+intros m s1; case s1; simpl; auto.
 intros H; injection H; intros H1; rewrite <- H1.
 intros p H0 H2; inversion H2.
 intros; discriminate.
 intros; discriminate.
 intros b s2' Rec n m s1.
-case n; simpl in |- *; auto.
+case n; simpl; auto.
 generalize (prefix_correct s1 (String b s2'));
  case (prefix s1 (String b s2')).
 intros H0 H; injection H; intros H1; rewrite <- H1; auto.
 intros p H2 H3; inversion H3.
-case m; simpl in |- *; auto.
+case m; simpl; auto.
 case (index 0 s1 s2'); intros; discriminate.
 intros m'; generalize (Rec 0 m' s1); case (index 0 s1 s2'); auto.
-intros x H H0 H1 p; try case p; simpl in |- *; auto.
-intros H2 H3; red in |- *; intros H4; case H0.
+intros x H H0 H1 p; try case p; simpl; auto.
+intros H2 H3; red; intros H4; case H0.
 intros H5 H6; absurd (false = true); auto with bool.
 intros n0 H2 H3; apply H; auto.
 injection H1; auto.
 apply Le.le_O_n.
 apply Lt.lt_S_n; auto.
 intros; discriminate.
-intros n'; case m; simpl in |- *; auto.
+intros n'; case m; simpl; auto.
 case (index n' s1 s2'); intros; discriminate.
 intros m'; generalize (Rec n' m' s1); case (index n' s1 s2'); auto.
-intros x H H0 p; case p; simpl in |- *; auto.
+intros x H H0 p; case p; simpl; auto.
 intros H1; inversion H1; auto.
 intros n0 H1 H2; apply H; auto.
 injection H0; auto.
@@ -312,33 +312,33 @@ Theorem index_correct3 :
  index n s1 s2 = None ->
  s1 <> EmptyString -> n <= m -> substring m (length s1) s2 <> s1.
 Proof.
-intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl in |- *;
+intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
  auto.
-intros n; case n; simpl in |- *; auto.
-intros m s1; case s1; simpl in |- *; auto.
-case m; intros; red in |- *; intros; discriminate.
+intros n; case n; simpl; auto.
+intros m s1; case s1; simpl; auto.
+case m; intros; red; intros; discriminate.
 intros n' m; case m; auto.
-intros s1; case s1; simpl in |- *; auto.
+intros s1; case s1; simpl; auto.
 intros b s2' Rec n m s1.
-case n; simpl in |- *; auto.
+case n; simpl; auto.
 generalize (prefix_correct s1 (String b s2'));
  case (prefix s1 (String b s2')).
 intros; discriminate.
-case m; simpl in |- *; auto with bool.
-case s1; simpl in |- *; auto.
-intros a s H H0 H1 H2; red in |- *; intros H3; case H.
+case m; simpl; auto with bool.
+case s1; simpl; auto.
+intros a s H H0 H1 H2; red; intros H3; case H.
 intros H4 H5; absurd (false = true); auto with bool.
-case s1; simpl in |- *; auto.
+case s1; simpl; auto.
 intros a s n0 H H0 H1 H2;
- change (substring n0 (length (String a s)) s2' <> String a s) in |- *;
+ change (substring n0 (length (String a s)) s2' <> String a s);
  apply (Rec 0); auto.
-generalize H0; case (index 0 (String a s) s2'); simpl in |- *; auto; intros;
+generalize H0; case (index 0 (String a s) s2'); simpl; auto; intros;
  discriminate.
 apply Le.le_O_n.
-intros n'; case m; simpl in |- *; auto.
+intros n'; case m; simpl; auto.
 intros H H0 H1; inversion H1.
 intros n0 H H0 H1; apply (Rec n'); auto.
-generalize H; case (index n' s1 s2'); simpl in |- *; auto; intros;
+generalize H; case (index n' s1 s2'); simpl; auto; intros;
  discriminate.
 apply Le.le_S_n; auto.
 Qed.
@@ -353,13 +353,13 @@ Theorem index_correct4 :
  forall (n : nat) (s : string),
  index n EmptyString s = None -> length s < n.
 Proof.
-intros n s; generalize n; clear n; elim s; simpl in |- *; auto.
-intros n; case n; simpl in |- *; auto.
+intros n s; generalize n; clear n; elim s; simpl; auto.
+intros n; case n; simpl; auto.
 intros; discriminate.
 intros; apply Lt.lt_O_Sn.
-intros a s' H n; case n; simpl in |- *; auto.
+intros a s' H n; case n; simpl; auto.
 intros; discriminate.
-intros n'; generalize (H n'); case (index n' EmptyString s'); simpl in |- *;
+intros n'; generalize (H n'); case (index n' EmptyString s'); simpl;
  auto.
 intros; discriminate.
 intros H0 H1; apply Lt.lt_n_S; auto.