Made option "Automatic Introduction" active by default before too many

people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 48 insertions, 48 deletions

diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index f11fb67b1..558d452bb 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -331,7 +331,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  Theorem Zgcd_div_pos a b:
    0 < b -> 0 < Zgcd a b -> 0 < b / Zgcd a b.
  Proof.
- intros a b Ha Hg.
+ intros Ha Hg.
  case (Zle_lt_or_eq 0 (b/Zgcd a b)); auto.
  apply Z_div_pos; auto with zarith.
  intros H; generalize Ha.
@@ -343,7 +343,7 @@ Theorem Zmod_le_first: forall a b, 0 <= a -> 0 < b -> 0 <= a mod b <= a.
  Theorem Zdiv_neg a b:
    a < 0 -> 0 < b -> a / b < 0.
  Proof.
- intros a b Ha Hb.
+ intros Ha Hb.
  assert (b > 0) by omega.
  generalize (Z_mult_div_ge a _ H); intros.
  assert (b * (a / b) < 0)%Z.
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index ca73a9f00..668fe83d6 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1877,14 +1877,14 @@ Section Int31_Specs.
 
  Lemma quotient_by_2 a: a - 1 <= (a/2) + (a/2).
  Proof.
- intros a; case (Z_mod_lt a 2); auto with zarith.
+ case (Z_mod_lt a 2); auto with zarith.
  intros H1; rewrite Zmod_eq_full; auto with zarith.
  Qed.
 
  Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k ->
    (j * k) + j <= ((j + k)/2 + 1)  ^ 2.
  Proof.
- intros j k Hj; generalize Hj k; pattern j; apply natlike_ind;
+ intros Hj; generalize Hj k; pattern j; apply natlike_ind;
    auto; clear k j Hj.
  intros _ k Hk; repeat rewrite Zplus_0_l.
  apply  Zmult_le_0_compat; generalize (Z_div_pos k 2); auto with zarith.
@@ -1907,7 +1907,7 @@ Section Int31_Specs.
 
  Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i/j))/2 + 1) ^ 2.
  Proof.
- intros i j Hi Hj.
+ intros Hi Hj.
  assert (Hij: 0 <= i/j) by (apply Z_div_pos; auto with zarith).
  apply Zlt_le_trans with (2 := sqrt_main_trick _ _ (Zlt_le_weak _ _ Hj) Hij).
  pattern i at 1; rewrite (Z_div_mod_eq i j); case (Z_mod_lt i j); auto with zarith.
@@ -1915,7 +1915,7 @@ Section Int31_Specs.
 
  Lemma sqrt_init i: 1 < i -> i < (i/2 + 1) ^ 2.
  Proof.
- intros i Hi.
+ intros Hi.
  assert (H1: 0 <= i - 2) by auto with zarith.
  assert (H2: 1 <= (i / 2) ^ 2); auto with zarith.
    replace i with (1* 2 + (i - 2)); auto with zarith.
@@ -1933,14 +1933,14 @@ Section Int31_Specs.
 
  Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i/j >= j -> j ^ 2 <= i.
  Proof.
- intros i j Hi Hj Hd; rewrite Zpower_2.
+ intros Hi Hj Hd; rewrite Zpower_2.
  apply Zle_trans with (j * (i/j)); auto with zarith.
  apply Z_mult_div_ge; auto with zarith.
  Qed.
 
  Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i/j < j ->  (j + (i/j))/2 < j.
  Proof.
- intros i j Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto.
+ intros Hi Hj H; case (Zle_or_lt j ((j + (i/j))/2)); auto.
  intros H1; contradict H; apply Zle_not_lt.
  assert (2 * j <= j + (i/j)); auto with zarith.
  apply Zle_trans with (2 * ((j + (i/j))/2)); auto with zarith.
@@ -1955,7 +1955,7 @@ Section Int31_Specs.
 
  Lemma Zcompare_spec i j: ZcompareSpec i j (i ?= j).
  Proof.
- intros i j; case_eq (Zcompare i j); intros H.
+ case_eq (Zcompare i j); intros H.
  apply ZcompareSpecEq; apply Zcompare_Eq_eq; auto.
  apply ZcompareSpecLt; auto.
  apply ZcompareSpecGt; apply Zgt_lt; auto.
@@ -1968,12 +1968,12 @@ Section Int31_Specs.
    | _ =>  j
    end.
  Proof.
- intros rec i j; unfold sqrt31_step; case div31; intros.
+ unfold sqrt31_step; case div31; intros.
  simpl; case compare31; auto.
  Qed.
 
  Lemma div31_phi i j: 0 < [|j|] -> [|fst (i/j)%int31|] = [|i|]/[|j|].
- intros i j Hj; generalize (spec_div i j Hj).
+ intros Hj; generalize (spec_div i j Hj).
  case div31; intros q r; simpl fst.
  intros (H1,H2); apply Zdiv_unique with [|r|]; auto with zarith.
  rewrite H1; ring.
@@ -1988,7 +1988,7 @@ Section Int31_Specs.
   [|sqrt31_step rec i j|] ^ 2 <= [|i|] < ([|sqrt31_step rec i j|] + 1) ^ 2.
  Proof.
  assert (Hp2: 0 < [|2|]) by exact (refl_equal Lt).
- intros rec i j Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def.
+ intros Hi Hj Hij H31 Hrec; rewrite sqrt31_step_def.
  rewrite spec_compare, div31_phi; auto.
    case Zcompare_spec; auto; intros Hc;
    try (split; auto; apply sqrt_test_true; auto with zarith; fail).
@@ -2024,7 +2024,7 @@ Section Int31_Specs.
        [|rec i j1|] ^ 2 <= [|i|] < ([|rec i j1|] + 1) ^ 2) ->
   [|iter31_sqrt n rec i j|] ^ 2 <= [|i|] < ([|iter31_sqrt n rec i j|] + 1) ^ 2.
  Proof.
- intros n; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n.
+ revert rec i j; elim n; unfold iter31_sqrt; fold iter31_sqrt; clear n.
  intros rec i j Hi Hj Hij H31 Hrec; apply sqrt31_step_correct; auto with zarith.
  intros; apply Hrec; auto with zarith.
  rewrite Zpower_0_r; auto with zarith.
@@ -2083,14 +2083,14 @@ Section Int31_Specs.
        end
    end.
  Proof.
- intros rec ih il j; unfold sqrt312_step; case div3121; intros.
+ unfold sqrt312_step; case div3121; intros.
  simpl; case compare31; auto.
  Qed.
 
  Lemma sqrt312_lower_bound ih il j:
    phi2 ih  il  < ([|j|] + 1) ^ 2 -> [|ih|] <= [|j|].
  Proof.
- intros ih il j H1.
+ intros H1.
  case (phi_bounded j); intros Hbj _.
  case (phi_bounded il); intros Hbil _.
  case (phi_bounded ih); intros Hbih Hbih1.
@@ -2104,7 +2104,7 @@ Section Int31_Specs.
  Lemma div312_phi ih il j: (2^30 <= [|j|] -> [|ih|] < [|j|] ->
   [|fst (div3121 ih il j)|] = phi2 ih il/[|j|])%Z.
  Proof.
- intros ih il j Hj Hj1.
+ intros Hj Hj1.
  generalize (spec_div21 ih il j Hj Hj1).
  case div3121; intros q r (Hq, Hr).
  apply Zdiv_unique with (phi r); auto with zarith.
@@ -2119,7 +2119,7 @@ Section Int31_Specs.
       < ([|sqrt312_step rec ih il j|] + 1) ^  2.
  Proof.
  assert (Hp2: (0 < [|2|])%Z) by exact (refl_equal Lt).
- intros rec ih il j Hih Hj Hij Hrec; rewrite sqrt312_step_def.
+ intros Hih Hj Hij Hrec; rewrite sqrt312_step_def.
  assert (H1: ([|ih|] <= [|j|])%Z) by (apply sqrt312_lower_bound with il; auto).
  case (phi_bounded ih); intros Hih1 _.
  case (phi_bounded il); intros Hil1 _.
@@ -2213,7 +2213,7 @@ Section Int31_Specs.
   [|iter312_sqrt n rec ih il j|] ^ 2 <= phi2 ih il
       < ([|iter312_sqrt n rec ih il j|] + 1) ^ 2.
  Proof.
- intros n; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n.
+ revert rec ih il j; elim n; unfold iter312_sqrt; fold iter312_sqrt; clear n.
  intros rec ih il j Hi Hj Hij Hrec; apply sqrt312_step_correct; auto with zarith.
  intros; apply Hrec; auto with zarith.
  rewrite Zpower_0_r; auto with zarith.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index c0b8074b6..2eb8584c9 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -105,7 +105,7 @@ Qed.
 Theorem spec_to_N n:
  ([n] = Zsgn [n] * (BigN.to_Z (BigZ.to_N n)))%Z.
 Proof.
-intros n; case n; simpl; intros p;
+case n; simpl; intros p;
   generalize (BigN.spec_pos p); case (BigN.to_Z p); auto.
 intros p1 H1; case H1; auto.
 intros p1 H1; case H1; auto.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 7afbee4a4..05508c4f3 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -45,7 +45,7 @@ Qed.
 
 Global Instance iter_wd (R:relation A) : Proper ((R==>R)==>eq==>R==>R) iter.
 Proof.
-intros R f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto.
+intros f f' Hf n n' Hn; subst n'. induction n; simpl; red; auto.
 Qed.
 
 End Iter.
@@ -412,4 +412,4 @@ Proof.
  rewrite ofnat_succ, pred_succ; auto with arith.
 Qed.
 
-End NZOfNatOps.
\ No newline at end of file
+End NZOfNatOps.
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index ba592507b..a5ef02570 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -110,7 +110,7 @@ Implicit Arguments recursion [A].
 Instance recursion_wd A (Aeq : relation A) :
  Proper (Aeq==>(eq==>Aeq==>Aeq)==>eq==>Aeq) (@recursion A).
 Proof.
-intros A Aeq a a' Eaa' f f' Eff'.
+intros a a' Eaa' f f' Eff'.
 intro x; pattern x; apply Nrect.
 intros x' H; now rewrite <- H.
 clear x.
@@ -200,4 +200,4 @@ end.
 Time Eval vm_compute in (binlog 500000). (* 0 sec *)
 Time Eval vm_compute in (binlog 1000000000000000000000000000000). (* 0 sec *)
 
-*)
\ No newline at end of file
+*)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 491c33666..5e3ecd688 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -126,7 +126,7 @@ Implicit Arguments recursion [A].
 Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
-intros A Aeq a a' Ha f f' Hf n n' Hn. subst n'.
+intros a a' Ha f f' Hf n n' Hn. subst n'.
 induction n; simpl; auto. apply Hf; auto.
 Qed.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 8cbd96c1f..f4641446b 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -200,7 +200,7 @@ Instance recursion_wd (A : Type) (Aeq : relation A) :
  Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A).
 Proof.
 unfold eq.
-intros A Aeq a a' Eaa' f f' Eff' x x' Exx'.
+intros a a' Eaa' f f' Eff' x x' Exx'.
 unfold recursion.
 unfold N.to_N.
 rewrite <- Exx'; clear x' Exx'.
diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 5022c9ae6..e2b63ebde 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -96,7 +96,7 @@ Definition predicate (A : Type) := A -> Prop.
 Instance well_founded_wd A :
  Proper (@relation_equivalence A ==> iff) (@well_founded A).
 Proof.
-intros A R1 R2 H.
+intros R1 R2 H.
 split; intros WF a; induction (WF a) as [x _ WF']; constructor;
 intros y Ryx; apply WF'; destruct (H y x); auto.
 Qed.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 6513922c4..407f7b90c 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -565,10 +565,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  ring.
  Qed.
 
- Instance strong_spec_mul_norm_Qz_Qq z n d
-   `(Reduced (Qq n d)) : Reduced (mul_norm_Qz_Qq z n d).
+ Instance strong_spec_mul_norm_Qz_Qq z n d :
+   forall `(Reduced (Qq n d)), Reduced (mul_norm_Qz_Qq z n d).
  Proof.
- unfold Reduced; intros z n d.
+ unfold Reduced.
  rewrite 2 strong_spec_red, 2 Qred_iff.
  simpl; nzsimpl.
  destr_eqb; intros Hd H; simpl in *; nzsimpl.
@@ -648,8 +648,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite <- Hg1, <- Hg2, <- Hg1', <- Hg2'; ring.
  Qed.
 
- Instance strong_spec_mul_norm x y
-  `(Reduced x, Reduced y) : Reduced (mul_norm x y).
+ Instance strong_spec_mul_norm x y :
+  forall `(Reduced x, Reduced y), Reduced (mul_norm x y).
  Proof.
  unfold Reduced; intros.
  rewrite strong_spec_red, Qred_iff.
@@ -833,7 +833,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  romega.
  Qed.
 
- Instance strong_spec_inv_norm x `(Reduced x) : Reduced (inv_norm x).
+ Instance strong_spec_inv_norm x : Reduced x -> Reduced (inv_norm x).
  Proof.
  unfold Reduced.
  intros.
@@ -888,7 +888,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_div x y: [div x y] == [x] / [y].
  Proof.
- intros x y; unfold div; rewrite spec_mul; auto.
+ unfold div; rewrite spec_mul; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv; auto.
@@ -898,7 +898,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_div_norm x y: [div_norm x y] == [x] / [y].
  Proof.
- intros x y; unfold div_norm; rewrite spec_mul_norm; auto.
+ unfold div_norm; rewrite spec_mul_norm; auto.
  unfold Qdiv; apply Qmult_comp.
  apply Qeq_refl.
  apply spec_inv_norm; auto.
@@ -1019,8 +1019,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite spec_inv_norm, spec_power_pos; apply Qeq_refl.
  Qed.
 
- Instance strong_spec_power_norm x z
-   `(Reduced x) : Reduced (power_norm x z).
+ Instance strong_spec_power_norm x z :
+   Reduced x -> Reduced (power_norm x z).
  Proof.
  destruct z; simpl.
  intros _; unfold Reduced; rewrite strong_spec_red.
@@ -1088,7 +1088,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_addc x y:
   [[add x y]] = [[x]] + [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1102,7 +1102,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_add_normc x y:
   [[add_norm x y]] = [[x]] + [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] + [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1125,14 +1125,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_subc x y:  [[sub x y]] = [[x]] - [[y]].
  Proof.
- intros x y; unfold sub; rewrite spec_addc; auto.
+ unfold sub; rewrite spec_addc; auto.
  rewrite spec_oppc; ring.
  Qed.
 
  Theorem spec_sub_normc x y:
    [[sub_norm x y]] = [[x]] - [[y]].
  Proof.
- intros x y; unfold sub_norm; rewrite spec_add_normc; auto.
+ unfold sub_norm; rewrite spec_add_normc; auto.
  rewrite spec_oppc; ring.
  Qed.
 
@@ -1150,7 +1150,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_mulc x y:
   [[mul x y]] = [[x]] * [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1164,7 +1164,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_mul_normc x y:
    [[mul_norm x y]] = [[x]] * [[y]].
  Proof.
- intros x y; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x] * [y])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1188,7 +1188,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_invc x:
    [[inv x]] =  /[[x]].
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1202,7 +1202,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_inv_normc x:
    [[inv_norm x]] =  /[[x]].
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! (/[x])).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1225,14 +1225,14 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]].
  Proof.
- intros x y; unfold div; rewrite spec_mulc; auto.
+ unfold div; rewrite spec_mulc; auto.
  unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
  apply spec_invc; auto.
  Qed.
 
  Theorem spec_div_normc x y: [[div_norm x y]] = [[x]] / [[y]].
  Proof.
- intros x y; unfold div_norm; rewrite spec_mul_normc; auto.
+ unfold div_norm; rewrite spec_mul_normc; auto.
  unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto.
  apply spec_inv_normc; auto.
  Qed.
@@ -1250,7 +1250,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
 
  Theorem spec_squarec x: [[square x]] = [[x]]^2.
  Proof.
- intros x; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x]^2)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.
@@ -1267,7 +1267,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  Theorem spec_power_posc x p:
    [[power_pos x p]] = [[x]] ^ nat_of_P p.
  Proof.
- intros x p; unfold to_Qc.
+ unfold to_Qc.
  apply trans_equal with (!! ([x]^Zpos p)).
  unfold Q2Qc.
  apply Qc_decomp; intros _ _; unfold this.