Merge PR #13649: Lint stdlib with -mangle-names #5

Reviewed-by: anton-trunov

21 files changed, 324 insertions, 313 deletions

diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v
index f002ee427c..dd10c758a5 100644
--- a/theories/Bool/BoolEq.v
+++ b/theories/Bool/BoolEq.v
@@ -46,7 +46,7 @@ Section Bool_eq_dec.
 
   Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}.
   Proof.
-    intros.
+    intros x y.
     exists (beq x y).
     constructor.
   Defined.
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index ef78121d63..5eb2a99739 100644
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -18,7 +18,7 @@ Theorem ifdec_left :
   forall (A B:Prop) (C:Set) (H:{A} + {B}),
     ~ B -> forall x y:C, ifdec H x y = x.
 Proof.
-  intros; case H; auto.
+  intros A B C H **; case H; auto.
   intro; absurd B; trivial.
 Qed.
 
@@ -26,7 +26,7 @@ Theorem ifdec_right :
   forall (A B:Prop) (C:Set) (H:{A} + {B}),
     ~ A -> forall x y:C, ifdec H x y = y.
 Proof.
-  intros; case H; auto.
+  intros A B C H **; case H; auto.
   intro; absurd A; trivial.
 Qed.
 
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 7e9087c377..8366e8257e 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -29,13 +29,13 @@ case diff_true_false; trivial with bool.
 Qed.
 
 Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A.
-intros.
+intros A B H.
 inversion H.
 assumption.
 Qed.
 
 Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B.
-intros.
+intros A B H.
 inversion H.
 assumption.
 Qed.
@@ -45,7 +45,7 @@ destruct 1; auto with bool.
 Qed.
 
 Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
-destruct b; intro H.
+intros A B b; destruct b; intro H.
 - left; inversion H; auto with bool.
 - right; inversion H; auto with bool.
 Qed.
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index aff5008410..418fc88489 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -19,26 +19,26 @@ Definition zerob (n:nat) : bool :=
     | S _ => false
   end.
 
-Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
+Lemma zerob_true_intro (n : nat) : n = 0 -> zerob n = true.
 Proof.
   destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 #[global]
 Hint Resolve zerob_true_intro: bool.
 
-Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
+Lemma zerob_true_elim (n : nat) : zerob n = true -> n = 0.
 Proof.
   destruct n; [ trivial with bool | inversion 1 ].
 Qed.
 
-Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
+Lemma zerob_false_intro (n : nat) : n <> 0 -> zerob n = false.
 Proof.
   destruct n; [ destruct 1; auto with bool | trivial with bool ].
 Qed.
 #[global]
 Hint Resolve zerob_false_intro: bool.
 
-Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
+Lemma zerob_false_elim (n : nat) : zerob n = false -> n <> 0.
 Proof.
   destruct n; [ inversion 1 | auto with bool ].
 Qed.
diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
index f23cf158ac..82a76e8afd 100644
--- a/theories/Classes/CEquivalence.v
+++ b/theories/Classes/CEquivalence.v
@@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
          now transitivity y.
   Qed.
 
-Arguments equiv_symmetric {A R} sa x y.
-Arguments equiv_transitive {A R} sa x y z.
+Arguments equiv_symmetric {A R} sa x y : rename.
+Arguments equiv_transitive {A R} sa x y z : rename.
 
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 9ff18ebe2c..d6a0ae5411 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -567,9 +567,7 @@ Section Normalize.
 
   Lemma proper_normalizes_proper `(Normalizes R0 R1, Proper A R1 m) : Proper R0 m.
   Proof.
-    red in H, H0. red in H.
-    apply (snd (H _ _)). 
-    assumption.
+    apply (_ : Normalizes R0 R1). assumption.
   Qed.
 
   Lemma flip_atom R : Normalizes R (flip (flip R)).
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index c489d82d0b..561822ef0c 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -352,14 +352,12 @@ Section Binary.
   Global Instance partial_order_antisym `(PartialOrder eqA R) : Antisymmetric eqA R.
   Proof with auto.
     reduce_goal.
-    apply H. firstorder.
+    firstorder.
   Qed.
 
   Lemma PartialOrder_inverse `(PartialOrder eqA R) : PartialOrder eqA (flip R).
   Proof.
-    unfold flip; constructor; unfold flip.
-    - intros X. apply H. apply symmetry. apply X.
-    - unfold relation_conjunction. intros [H1 H2]. apply H. constructor; assumption.
+    firstorder.
   Qed.
 End Binary.
 
diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v
index 7169aa673d..cd6765bab9 100644
--- a/theories/Classes/DecidableClass.v
+++ b/theories/Classes/DecidableClass.v
@@ -46,7 +46,7 @@ Qed.
 (** The generic function that should be used to program, together with some
   useful tactics. *)
 
-Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
+Definition decide P {H : Decidable P} := @Decidable_witness _ H.
 
 Ltac _decide_ P H :=
   let b := fresh "b" in
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index d96bd72561..4d9069b4d0 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -64,8 +64,8 @@ Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
          now transitivity y.
   Qed.
 
-Arguments equiv_symmetric {A R} sa x y.
-Arguments equiv_transitive {A R} sa x y z.
+Arguments equiv_symmetric {A R} sa x y : rename.
+Arguments equiv_transitive {A R} sa x y z : rename.
 
 (** Use the [substitute] command which substitutes an equivalence in every hypothesis. *)
 
diff --git a/theories/Logic/FunctionalExtensionality.v b/theories/Logic/FunctionalExtensionality.v
index e9d434b488..ae1d978bfb 100644
--- a/theories/Logic/FunctionalExtensionality.v
+++ b/theories/Logic/FunctionalExtensionality.v
@@ -16,7 +16,7 @@
 Lemma equal_f : forall {A B : Type} {f g : A -> B},
   f = g -> forall x, f x = g x.
 Proof.
-  intros.
+  intros A B f g H x.
   rewrite H.
   auto.
 Qed.
@@ -118,7 +118,7 @@ Definition f_equal__functional_extensionality_dep_good
            {A B f g} H a
   : f_equal (fun h => h a) (@functional_extensionality_dep_good A B f g H) = H a.
 Proof.
-  apply forall_eq_rect with (H := H); clear H g.
+  apply (fun P k => forall_eq_rect _ P k _ H); clear H g.
   change (eq_refl (f a)) with (f_equal (fun h => h a) (eq_refl f)).
   apply f_equal, functional_extensionality_dep_good_refl.
 Defined.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 7ee3a99d60..21eed3a696 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -39,8 +39,8 @@ Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
 Register JMeq_hom as core.JMeq.hom.
 
 Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
-Proof. 
-intros; destruct H; trivial.
+Proof.
+intros A B x y H; destruct H; trivial.
 Qed.
 
 #[global]
@@ -150,7 +150,7 @@ Lemma JMeq_eq_dep :
   forall U (P:U->Type) p q (x:P p) (y:P q), 
   p = q -> JMeq x y -> eq_dep U P p x q y.
 Proof.
-intros.
+intros U P p q x y H H0.
 destruct H.
 apply JMeq_eq in H0 as ->.
 reflexivity.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index c469a49903..f324bbf52b 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -226,7 +226,7 @@ Proof.
   apply Z.lt_le_trans with (1:= H5); auto with zarith.
   apply Zpower_le_monotone; auto with zarith.
   rewrite Zplus_mod; auto with zarith.
-  rewrite -> Zmod_small with (a := t); auto with zarith.
+  rewrite -> (Zmod_small t); auto with zarith.
   apply Zmod_small; auto with zarith.
   split; auto with zarith.
   assert (0 <= 2 ^a * r); auto with zarith.
@@ -489,15 +489,15 @@ Definition cast i j :=
 
 Lemma cast_refl : forall i, cast i i = Some (fun P H => H).
 Proof.
- unfold cast;intros.
+ unfold cast;intros i.
  generalize (eqb_correct i i).
- rewrite eqb_refl;intros.
+ rewrite eqb_refl;intros e.
  rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial.
 Qed.
 
 Lemma cast_diff : forall i j, i =? j = false -> cast i j = None.
 Proof.
- intros;unfold cast;intros; generalize (eqb_correct i j).
+ intros i j H;unfold cast;intros; generalize (eqb_correct i j).
  rewrite H;trivial.
 Qed.
 
@@ -509,15 +509,15 @@ Definition eqo i j :=
 
 Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i).
 Proof.
- unfold eqo;intros.
+ unfold eqo;intros i.
  generalize (eqb_correct i i).
- rewrite eqb_refl;intros.
+ rewrite eqb_refl;intros e.
  rewrite (Eqdep_dec.eq_proofs_unicity eq_dec (e (eq_refl true)) (eq_refl i));trivial.
 Qed.
 
 Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None.
 Proof.
- unfold eqo;intros; generalize (eqb_correct i j).
+ unfold eqo;intros i j H; generalize (eqb_correct i j).
  rewrite H;trivial.
 Qed.
 
@@ -651,7 +651,7 @@ Proof.
  apply Zgcdn_is_gcd.
  unfold Zgcd_bound.
  generalize (to_Z_bounded b).
- destruct φ b.
+ destruct φ b as [|p|p].
  unfold size; auto with zarith.
  intros (_,H).
  cut (Psize p <= size)%nat; [ lia | rewrite <- Zpower2_Psize; auto].
@@ -727,7 +727,7 @@ Proof.
      replace ((φ m + φ n) mod wB)%Z with ((((φ m + φ n) - wB) + wB) mod wB)%Z.
      rewrite -> Zplus_mod, Z_mod_same_full, Zplus_0_r, !Zmod_small; auto with zarith.
      rewrite !Zmod_small; auto with zarith.
-     apply f_equal2 with (f := Zmod); auto with zarith.
+     apply (f_equal2 Zmod); auto with zarith.
    case_eq (n <=? m + n)%int63; auto.
    rewrite leb_spec, H1; auto with zarith.
  assert (H1: (φ (m + n)  = φ m + φ n)%Z).
@@ -805,7 +805,7 @@ Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%int63.
 Proof.
  apply to_Z_inj; rewrite -> !lsl_spec, !add_spec, Zmult_mod_idemp_l.
  rewrite -> !lsl_spec, <-Zplus_mod.
- apply f_equal2 with (f := Zmod); auto with zarith.
+ apply (f_equal2 Zmod); auto with zarith.
 Qed.
 
 Lemma lsr_M_r x i (H: (digits <=? i = true)%int63) : x >> i = 0%int63.
@@ -973,14 +973,14 @@ Proof.
  case H2; intros _ H3; case (Zle_or_lt φ i φ j); intros F2.
    2: generalize (H3 F2); discriminate.
  clear H2 H3.
- apply f_equal with (f := negb).
- apply f_equal with (f := is_zero).
+ apply (f_equal negb).
+ apply (f_equal is_zero).
  apply to_Z_inj.
  rewrite -> !lsl_spec, !lsr_spec, !lsl_spec.
  pattern wB at 2 3; replace wB with (2^(1+ φ (digits - 1))); auto.
  rewrite -> Zpower_exp, Z.pow_1_r; auto with zarith.
  rewrite !Zmult_mod_distr_r.
- apply f_equal2 with (f := Zmult); auto.
+ apply (f_equal2 Zmult); auto.
  replace wB with (2^ d); auto with zarith.
  replace d with ((d - φ i) + φ i)%Z by ring.
  case (to_Z_bounded i); intros  H1i H2i.
@@ -1078,8 +1078,8 @@ Proof.
  2: generalize (Hn 0%int63); do 2 case bit; auto; intros [ ]; auto.
  rewrite lsl_add_distr.
  rewrite (bit_split x) at 1; rewrite (bit_split y) at 1.
- rewrite <-!add_assoc; apply f_equal2 with (f := add); auto.
- rewrite add_comm, <-!add_assoc; apply f_equal2 with (f := add); auto.
+ rewrite <-!add_assoc; apply (f_equal2 add); auto.
+ rewrite add_comm, <-!add_assoc; apply (f_equal2 add); auto.
  rewrite add_comm; auto.
  intros Heq.
  generalize (add_le_r x y); rewrite Heq, lor_le; intro Hb.
@@ -1360,7 +1360,7 @@ Lemma sqrt2_step_def rec ih il j:
     else j
    else j.
 Proof.
- unfold sqrt2_step; case diveucl_21; intros;simpl.
+ unfold sqrt2_step; case diveucl_21; intros i j';simpl.
  case (j +c i);trivial.
 Qed.
 
@@ -1390,7 +1390,7 @@ Proof.
  assert (W1:= to_Z_bounded a1).
  assert (W2:= to_Z_bounded a2).
  assert (Wb:= to_Z_bounded b).
- assert (φ b>0) by (auto with zarith).
+ assert (φ b>0) as H by (auto with zarith).
  generalize (Z_div_mod (φ a1*wB+φ a2) φ b H).
  revert W.
  destruct (diveucl_21 a1 a2 b); destruct (Z.div_eucl (φ a1*wB+φ a2) φ b).
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index d1be8812e9..69873d0321 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -43,7 +43,7 @@ Section Well_founded.
     forall (x:A) (r:Acc R x),
       F_sub x (fun y:{y:A | R y x} => Fix_F_sub (`y) (Acc_inv r (proj2_sig y))) = Fix_F_sub x r.
   Proof.
-    destruct r using Acc_inv_dep; auto.
+    intros x r; destruct r using Acc_inv_dep; auto.
   Qed.
 
   Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F_sub x r = Fix_F_sub x s.
@@ -95,12 +95,12 @@ Section Measure_well_founded.
   Proof with auto.
     unfold well_founded.
     cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
-    + intros.
+    + intros H a.
       apply (H (m a))...
     + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
-      intros.
+      intros ? H ? H0.
       apply Acc_intro.
-      intros.
+      intros y H1.
       unfold MR in H1.
       rewrite H0 in H1.
       apply (H (m y))...
@@ -174,7 +174,7 @@ Section Fix_rects.
     revert a'.
     pattern x, (Fix_F_sub A R P f x a).
     apply Fix_F_sub_rect.
-    intros.
+    intros ? H **.
     rewrite F_unfold.
     apply equiv_lowers.
     intros.
@@ -197,11 +197,11 @@ Section Fix_rects.
     : forall x, Q _ (Fix_sub A R Rwf P f x).
   Proof with auto.
     unfold Fix_sub.
-    intros.
+    intros x.
     apply Fix_F_sub_rect.
-    intros.
-    assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))...
-    set (inv x0 X0 a). clearbody q.
+    intros x0 H a.
+    assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y))) as X0...
+    set (q := inv x0 X0 a). clearbody q.
     rewrite <- (equiv_lowers (fun y: {y: A | R y x0} =>
       Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y)))
     (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
@@ -242,9 +242,9 @@ Module WfExtensionality.
         Fix_sub A R Rwf P F_sub x =
           F_sub x (fun y:{y : A | R y x} => Fix_sub A R Rwf P F_sub (` y)).
   Proof.
-    intros ; apply Fix_eq ; auto.
-    intros.
-    assert(f = g).
+    intros A R Rwf P F_sub x; apply Fix_eq ; auto.
+    intros ? f g H.
+    assert(f = g) as H0.
     - extensionality y ; apply H.
     - rewrite H0 ; auto.
   Qed.
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index b008c6c2aa..4e596a165c 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -637,13 +637,13 @@ Qed.
 
 Lemma Qmult_1_l : forall n, 1*n == n.
 Proof.
-  intro; red; simpl; destruct (Qnum n); auto.
+  intro n; red; simpl; destruct (Qnum n); auto.
 Qed.
 
 Theorem Qmult_1_r : forall n, n*1==n.
 Proof.
-  intro; red; simpl.
-  rewrite Z.mul_1_r with (n := Qnum n).
+  intro n; red; simpl.
+  rewrite (Z.mul_1_r (Qnum n)).
   rewrite Pos.mul_comm; simpl; trivial.
 Qed.
 
@@ -709,7 +709,7 @@ Qed.
 Theorem Qmult_inv_r : forall x, ~ x == 0 -> x*(/x) == 1.
 Proof.
   intros (x1, x2); unfold Qeq, Qdiv, Qmult; case x1; simpl;
-    intros; simpl_mult; try ring.
+    intros H **; simpl_mult; try ring.
   elim H; auto.
 Qed.
 
@@ -722,7 +722,7 @@ Qed.
 
 Theorem Qdiv_mult_l : forall x y, ~ y == 0 -> (x*y)/y == x.
 Proof.
-  intros; unfold Qdiv.
+  intros x y H; unfold Qdiv.
   rewrite <- (Qmult_assoc x y (Qinv y)).
   rewrite (Qmult_inv_r y H).
   apply Qmult_1_r.
@@ -730,7 +730,7 @@ Qed.
 
 Theorem Qmult_div_r : forall x y, ~ y == 0 -> y*(x/y) == x.
 Proof.
-  intros; unfold Qdiv.
+  intros x y ?; unfold Qdiv.
   rewrite (Qmult_assoc y x (Qinv y)).
   rewrite (Qmult_comm y x).
   fold (Qdiv (Qmult x y) y).
@@ -845,7 +845,7 @@ Qed.
 
 Lemma Qlt_trans : forall x y z, x<y -> y<z -> x<z.
 Proof.
-  intros.
+  intros x y z ? ?.
   apply Qle_lt_trans with y; auto.
   apply Qlt_le_weak; auto.
 Qed.
@@ -877,19 +877,19 @@ Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le
 
 Lemma Q_dec : forall x y, {x<y} + {y<x} + {x==y}.
 Proof.
-  unfold Qlt, Qle, Qeq; intros.
+  unfold Qlt, Qle, Qeq; intros x y.
   exact (Z_dec' (Qnum x * QDen y) (Qnum y * QDen x)).
 Defined.
 
 Lemma Qlt_le_dec : forall x y, {x<y} + {y<=x}.
 Proof.
-  unfold Qlt, Qle; intros.
+  unfold Qlt, Qle; intros x y.
   exact (Z_lt_le_dec (Qnum x * QDen y) (Qnum y * QDen x)).
 Defined.
 
 Lemma Qarchimedean : forall q : Q, { p : positive | q < Z.pos p # 1 }.
 Proof.
-  intros. destruct q as [a b]. destruct a.
+  intros q. destruct q as [a b]. destruct a as [|p|p].
   - exists xH. reflexivity.
   - exists (p+1)%positive. apply (Z.lt_le_trans _ (Z.pos (p+1))).
     simpl. rewrite Pos.mul_1_r.
@@ -1169,12 +1169,12 @@ Qed.
 Lemma Qinv_lt_contravar : forall a b : Q,
     0 < a -> 0 < b -> (a < b <-> /b < /a).
 Proof.
-  intros. split.
-  - intro. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0.
+  intros a b H H0. split.
+  - intro H1. rewrite <- Qmult_1_l. apply Qlt_shift_div_r. apply H0.
     rewrite <- (Qmult_inv_r a). rewrite Qmult_comm.
     apply Qmult_lt_l. apply Qinv_lt_0_compat.  apply H.
     apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H).
-  - intro. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)).
+  - intro H1. rewrite <- (Qinv_involutive b). rewrite <- (Qmult_1_l (// b)).
     apply Qlt_shift_div_l. apply Qinv_lt_0_compat. apply H0.
     rewrite <- (Qmult_inv_r a). apply Qmult_lt_l. apply H.
     apply H1. intro abs. rewrite abs in H. apply (Qlt_irrefl 0 H).
@@ -1190,7 +1190,7 @@ Instance Qpower_positive_comp : Proper (Qeq==>eq==>Qeq) Qpower_positive.
 Proof.
 intros x x' Hx y y' Hy. rewrite <-Hy; clear y' Hy.
 unfold Qpower_positive.
-induction y; simpl;
+induction y as [y IHy|y IHy|]; simpl;
 try rewrite IHy;
 try rewrite Hx;
 reflexivity.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index 533c675415..e94ae1e789 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -129,19 +129,19 @@ Qed.
 
 Add Morphism Qplus' with signature (Qeq ==> Qeq ==> Qeq) as Qplus'_comp.
 Proof.
-  intros; unfold Qplus'.
+  intros ? ? H ? ? H0; unfold Qplus'.
   rewrite H, H0; auto with qarith.
 Qed.
 
 Add Morphism Qmult' with signature (Qeq ==> Qeq ==> Qeq) as Qmult'_comp.
 Proof.
-  intros; unfold Qmult'.
+  intros ? ? H ? ? H0; unfold Qmult'.
   rewrite H, H0; auto with qarith.
 Qed.
 
 Add Morphism Qminus' with signature (Qeq ==> Qeq ==> Qeq) as Qminus'_comp.
 Proof.
-  intros; unfold Qminus'.
+  intros ? ? H ? ? H0; unfold Qminus'.
   rewrite H, H0; auto with qarith.
 Qed.
 
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 9a1bbca99f..c11077607e 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -58,9 +58,9 @@ Open Scope Z_scope.
  Lemma Zgcdn_pos : forall n a b,
    0 <= Zgcdn n a b.
  Proof.
-   induction n.
+   intros n; induction n.
    simpl; auto with zarith.
-   destruct a; simpl; intros; auto with zarith; auto.
+   intros a; destruct a; simpl; intros; auto with zarith; auto.
  Qed.
 
  Lemma Zgcd_alt_pos : forall a b, 0 <= Zgcd_alt a b.
@@ -75,9 +75,9 @@ Open Scope Z_scope.
  Lemma Zgcdn_linear_bound : forall n a b,
    Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b).
  Proof.
-   induction n.
+   intros n; induction n as [|n IHn].
    intros; lia.
-   destruct a; intros; simpl;
+   intros a; destruct a as [|p|p]; intros b H; simpl;
      [ generalize (Zis_gcd_0_abs b); intuition | | ];
    unfold Z.modulo;
    generalize (Z_div_mod b (Zpos p) (eq_refl Gt));
@@ -106,7 +106,7 @@ Open Scope Z_scope.
  Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
  Proof.
    enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto.
-   induction N. intros; lia.
+   intros N; induction N as [|N IHN]. intros; lia.
    intros [ | [ | n ] ]. 1-2: simpl; lia.
    intros.
    change (0 <= fibonacci (S n) + fibonacci n).
@@ -116,11 +116,11 @@ Open Scope Z_scope.
  Lemma fibonacci_incr :
    forall n m, (n<=m)%nat -> fibonacci n <= fibonacci m.
  Proof.
-   induction 1.
+   induction 1 as [|m H IH].
    auto with zarith.
    apply Z.le_trans with (fibonacci m); auto.
    clear.
-   destruct m.
+   destruct m as [|m].
    simpl; auto with zarith.
    change (fibonacci (S m) <= fibonacci (S m)+fibonacci m).
    generalize (fibonacci_pos m); lia.
@@ -137,10 +137,10 @@ Open Scope Z_scope.
    fibonacci (S n) <= a /\
    fibonacci (S (S n)) <= b.
  Proof.
-   induction n.
+   intros n; induction n as [|n IHn].
    intros [|a|a]; intros; simpl; lia.
    intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ].
-   remember (S n) as m.
+   remember (S n) as m eqn:Heqm.
    rewrite Heqm at 2. simpl Zgcdn.
    unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl).
    destruct (Z.div_eucl b (Zpos a)) as (q,r).
@@ -171,19 +171,19 @@ Open Scope Z_scope.
    0 < a < b -> a < fibonacci (S n) ->
    Zis_gcd a b (Zgcdn n a b).
  Proof.
-   destruct a. 1,3 : intros; lia.
+   intros n a; destruct a as [|p|p]. 1,3 : intros; lia.
    cut (forall k n b,
      k = (S (Pos.to_nat p) - n)%nat ->
      0 < Zpos p < b -> Zpos p < fibonacci (S n) ->
      Zis_gcd (Zpos p) b (Zgcdn n (Zpos p) b)).
    destruct 2; eauto.
-   clear n; induction k.
+   clear n; intros k; induction k as [|k IHk].
    intros.
    apply Zgcdn_linear_bound.
    lia.
-   intros.
-   generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros.
-   assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)).
+   intros n b H H0 H1.
+   generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros H2.
+   assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)) as H3.
    apply IHk; auto.
    lia.
    replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto.
@@ -197,13 +197,13 @@ Open Scope Z_scope.
  Lemma Zgcd_bound_fibonacci :
    forall a, 0 < a -> a < fibonacci (Zgcd_bound a).
  Proof.
-   destruct a; [lia| | intro H; discriminate].
+   intros a; destruct a as [|p|p]; [lia| | intro H; discriminate].
    intros _.
-   induction p; [ | | compute; auto ];
+   induction p as [p IHp|p IHp|]; [ | | compute; auto ];
     simpl Zgcd_bound in *;
     rewrite plus_comm; simpl plus;
     set (n:= (Pos.size_nat p+Pos.size_nat p)%nat) in *; simpl;
-    assert (n <> O) by (unfold n; destruct p; simpl; auto).
+    assert (n <> O) as H by (unfold n; destruct p; simpl; auto).
 
    destruct n as [ |m]; [elim H; auto| ].
    generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia.
@@ -229,11 +229,11 @@ Open Scope Z_scope.
  Lemma Zgcdn_is_gcd_pos n a b : (Zgcd_bound (Zpos a) <= n)%nat ->
    Zis_gcd (Zpos a) b (Zgcdn n (Zpos a) b).
  Proof.
-  intros.
+  intros H.
   generalize (Zgcd_bound_fibonacci (Zpos a)).
   simpl Zgcd_bound in *.
-  remember (Pos.size_nat a+Pos.size_nat a)%nat as m.
-  assert (1 < m)%nat.
+  remember (Pos.size_nat a+Pos.size_nat a)%nat as m eqn:Heqm.
+  assert (1 < m)%nat as H0.
   { rewrite Heqm; destruct a; simpl; rewrite 1?plus_comm;
     auto with arith. }
   destruct m as [ |m]; [inversion H0; auto| ].
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index b69af424b1..bc3f5706c9 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -83,10 +83,10 @@ Proof. intros. apply Z.lt_le_incl. now apply Z.pow_gt_lin_r. Qed.
 Lemma Zpower2_Psize n p :
   Zpos p < 2^(Z.of_nat n) <-> (Pos.size_nat p <= n)%nat.
 Proof.
-  revert p; induction n.
-  destruct p; now split.
+  revert p; induction n as [|n IHn].
+  intros p; destruct p; now split.
   assert (Hn := Nat2Z.is_nonneg n).
-  destruct p; simpl Pos.size_nat.
+  intros p; destruct p as [p|p|]; simpl Pos.size_nat.
   - specialize IHn with p.
     rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia.
   - specialize IHn with p.
@@ -138,7 +138,7 @@ Definition Zpow_mod a m n :=
 Theorem Zpow_mod_pos_correct a m n :
  n <> 0 -> Zpow_mod_pos a m n = (Z.pow_pos a m) mod n.
 Proof.
-  intros Hn. induction m.
+  intros Hn. induction m as [m IHm|m IHm|].
   - rewrite Pos.xI_succ_xO at 2. rewrite <- Pos.add_1_r, <- Pos.add_diag.
     rewrite 2 Zpower_pos_is_exp, Zpower_pos_1_r.
     rewrite Z.mul_mod, (Z.mul_mod (Z.pow_pos a m)) by trivial.
@@ -193,7 +193,7 @@ Proof.
     assert (p<=1) by (apply Z.divide_pos_le; auto with zarith).
     lia.
   - intros n Hn Rec.
-    rewrite Z.pow_succ_r by trivial. intros.
+    rewrite Z.pow_succ_r by trivial. intros H.
     assert (2<=p) by (apply prime_ge_2; auto).
     assert (2<=q) by (apply prime_ge_2; auto).
     destruct prime_mult with (2 := H); auto.
@@ -229,7 +229,7 @@ Proof.
   (* x = 1 *)
   exists 0; rewrite Z.pow_0_r; auto.
   (* x = 0 *)
-  exists n; destruct H; rewrite Z.mul_0_r in H; auto.
+  exists n; destruct H as [? H]; rewrite Z.mul_0_r in H; auto.
 Qed.
 
 (** * Z.square: a direct definition of [z^2] *)
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 6f464d89bb..6b01d798e4 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp :
   forall (n m:nat) (z:Z),
     Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.
 Proof.
- induction n.
+ intros n; induction n as [|n IHn].
  - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l.
  - intros. simpl. now rewrite IHn, Z.mul_assoc.
 Qed.
@@ -135,7 +135,7 @@ Section Powers_of_2.
 
   Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).
   Proof.
-   induction n.
+   induction n as [|n IHn].
    - trivial.
    - now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg.
   Qed.
@@ -164,7 +164,7 @@ Section Powers_of_2.
   Theorem shift_nat_correct n x :
     Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.
   Proof.
-   induction n.
+   induction n as [|n IHn].
    - trivial.
    - now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn.
   Qed.
@@ -295,7 +295,7 @@ Section power_div_with_rest.
      rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc.
      repeat split; auto.
      rewrite !Z.mul_1_l, H, Z.add_assoc.
-     apply f_equal2 with (f := Z.add); auto.
+     apply (f_equal2 Z.add); auto.
      rewrite <- Z.sub_sub_distr, <- !Z.add_diag, Z.add_simpl_r.
      now rewrite Z.mul_1_l.
    - rewrite Pos2Z.neg_xO in H.
@@ -303,7 +303,7 @@ Section power_div_with_rest.
      repeat split; auto.
    - repeat split; auto.
      rewrite H, (Z.mul_opp_l 1), Z.mul_1_l, Z.add_assoc.
-     apply f_equal2 with (f := Z.add); auto.
+     apply (f_equal2 Z.add); auto.
      rewrite Z.add_comm, <- Z.add_diag.
      rewrite Z.mul_add_distr_l.
      replace (-1 * d) with (-d).
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index 515372466a..e4129f8382 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -1371,13 +1371,13 @@ Section S.
     destruct pol;auto.
     generalize (is_cnf_tt_inv (xcnf (negb true) f1)).
     destruct (is_cnf_tt (xcnf (negb true) f1)).
-    + intros.
+    + intros H.
       rewrite H by auto.
       reflexivity.
     +
       generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
     destruct (is_cnf_ff (xcnf (negb true) f1)).
-    * intros.
+    * intros H.
       rewrite H by auto.
       unfold or_cnf_opt.
       simpl.
diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v
index 1616b5a2a4..a4b631fc13 100644
--- a/theories/micromega/ZMicromega.v
+++ b/theories/micromega/ZMicromega.v
@@ -38,7 +38,7 @@ Ltac inv H := inversion H ; try subst ; clear H.
 Lemma eq_le_iff : forall x, 0 = x  <-> (0 <= x /\ x <= 0).
 Proof.
   intros.
-  split ; intros.
+  split ; intros H.
   - subst.
     compute. intuition congruence.
   - destruct H.
@@ -48,7 +48,7 @@ Qed.
 Lemma lt_le_iff : forall x,
     0 < x <-> 0 <= x - 1.
 Proof.
-  split ; intros.
+  split ; intros H.
   - apply Zlt_succ_le.
     ring_simplify.
     auto.
@@ -70,12 +70,13 @@ Lemma le_neg : forall x,
 Proof.
   intro.
   rewrite lt_le_iff.
-  split ; intros.
+  split ; intros H.
   - apply Znot_le_gt in H.
     apply Zgt_le_succ in H.
     rewrite le_0_iff in H.
     ring_simplify in H; auto.
-  - assert (C := (Z.add_le_mono _ _ _ _ H H0)).
+  - intro H0.
+    assert (C := (Z.add_le_mono _ _ _ _ H H0)).
     ring_simplify in C.
     compute in C.
     apply C ; reflexivity.
@@ -84,7 +85,7 @@ Qed.
 Lemma eq_cnf : forall x,
     (0 <= x - 1 -> False) /\ (0 <= -1 - x -> False) <-> x = 0.
 Proof.
-  intros.
+  intros x.
   rewrite Z.eq_sym_iff.
   rewrite eq_le_iff.
   rewrite (le_0_iff x 0).
@@ -108,7 +109,7 @@ Proof.
   auto using Z.le_antisymm.
   eauto using Z.le_trans.
   apply Z.le_neq.
-  destruct (Z.lt_trichotomy n m) ; intuition.
+  apply Z.lt_trichotomy.
   apply Z.add_le_mono_l; assumption.
   apply Z.mul_pos_pos ; auto.
   discriminate.
@@ -160,18 +161,18 @@ Fixpoint Zeval_const  (e: PExpr Z) : option Z :=
 
 Lemma ZNpower : forall r n, r ^ Z.of_N n = pow_N 1 Z.mul r n.
 Proof.
-  destruct n.
+  intros r n; destruct n as [|p].
   reflexivity.
   simpl.
   unfold Z.pow_pos.
   replace (pow_pos Z.mul r p) with (1 * (pow_pos Z.mul r p)) by ring.
   generalize 1.
-  induction p; simpl ; intros ; repeat rewrite IHp ; ring.
+  induction p as [p IHp|p IHp|]; simpl ; intros ; repeat rewrite IHp ; ring.
 Qed.
 
 Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e.
 Proof.
-  induction e ; simpl ; try congruence.
+  intros env e; induction e ; simpl ; try congruence.
   reflexivity.
   rewrite ZNpower. congruence.
 Qed.
@@ -201,7 +202,7 @@ Lemma pop2_bop2 :
   forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2.
 Proof.
   unfold is_true.
-  destruct op ; simpl; intros.
+  intro op; destruct op ; simpl; intros q1 q2.
   - apply Z.eqb_eq.
   - rewrite <- Z.eqb_eq.
     rewrite negb_true_iff.
@@ -220,7 +221,7 @@ Definition Zeval_op2 (k: Tauto.kind) :  Op2 ->  Z -> Z -> Tauto.rtyp k:=
 Lemma Zeval_op2_hold : forall k op q1 q2,
     Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2.
 Proof.
-  destruct k.
+  intro k; destruct k.
   simpl ; tauto.
   simpl. apply pop2_bop2.
 Qed.
@@ -235,18 +236,18 @@ Definition Zeval_formula' :=
 
 Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f.
 Proof.
-  destruct k ; simpl.
+  intros env k; destruct k ; simpl.
   - tauto.
-  - destruct f ; simpl.
-    rewrite <- Zeval_op2_hold with (k:=Tauto.isBool).
+  - intros f; destruct f ; simpl.
+    rewrite <- (Zeval_op2_hold Tauto.isBool).
     simpl. tauto.
 Qed.
 
 Lemma Zeval_formula_compat' : forall env f,  Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f.
 Proof.
-  intros.
+  intros env f.
   unfold Zeval_formula.
-  destruct f.
+  destruct f as [Flhs  Fop Frhs].
   repeat rewrite Zeval_expr_compat.
   unfold Zeval_formula' ; simpl.
   unfold eval_expr.
@@ -343,7 +344,7 @@ Lemma Zunsat_sound : forall f,
     Zunsat f = true -> forall env, eval_nformula env f -> False.
 Proof.
   unfold Zunsat.
-  intros.
+  intros f H env ?.
   destruct f.
   eapply check_inconsistent_sound with (1 := Zsor) (2 := ZSORaddon) in H; eauto.
 Qed.
@@ -365,7 +366,7 @@ Lemma xnnormalise_correct :
   forall env f,
     eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f.
 Proof.
-  intros.
+  intros env f.
   rewrite Zeval_formula_compat'.
   unfold xnnormalise.
   destruct f as [lhs o rhs].
@@ -375,18 +376,18 @@ Proof.
       generalize (   eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
                                  (fun x : N => x) (pow_N 1 Z.mul) env lhs);
       generalize (eval_pexpr  Z.add Z.mul Z.sub Z.opp (fun x : Z => x)
-                              (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros.
+                              (fun x : N => x) (pow_N 1 Z.mul) env rhs); intros z z0.
   - split ; intros.
-    + assert (z0 + (z - z0) = z0 + 0) by congruence.
+    + assert (z0 + (z - z0) = z0 + 0) as H0 by congruence.
       rewrite Z.add_0_r in H0.
       rewrite <- H0.
       ring.
     + subst.
       ring.
-  - split ; repeat intro.
+  - split ; intros H H0.
     subst. apply H. ring.
     apply H.
-    assert (z0 + (z - z0) = z0 + 0) by congruence.
+    assert (z0 + (z - z0) = z0 + 0) as H1 by congruence.
     rewrite Z.add_0_r in H1.
     rewrite <- H1.
     ring.
@@ -396,11 +397,11 @@ Proof.
   - split ; intros.
     + apply Zle_0_minus_le; auto.
     + apply Zle_minus_le_0; auto.
-  - split ; intros.
+  - split ; intros H.
     + apply Zlt_0_minus_lt; auto.
     + apply Zlt_left_lt in H.
       apply H.
-  - split ; intros.
+  - split ; intros H.
     + apply Zlt_0_minus_lt ; auto.
     + apply Zlt_left_lt in H.
       apply H.
@@ -430,7 +431,7 @@ Ltac iff_ring :=
 Lemma xnormalise_correct : forall env f,
     (make_conj (fun x => eval_nformula env x -> False) (xnormalise f)) <-> eval_nformula env f.
 Proof.
-  intros.
+  intros env f.
   destruct f as [e o]; destruct o eqn:Op; cbn - [psub];
     repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc;
       generalize (eval_pol env e) as x; intro.
@@ -458,11 +459,11 @@ Lemma cnf_of_list_correct :
   make_conj (fun x : NFormula Z => eval_nformula env x -> False) f.
 Proof.
   unfold cnf_of_list.
-  intros.
+  intros T tg f env.
   set (F := (fun (x : NFormula Z) (acc : list (list (NFormula Z * T))) =>
         if Zunsat x then acc else ((x, tg) :: nil) :: acc)).
   set (E := ((fun x : NFormula Z => eval_nformula env x -> False))).
-  induction f.
+  induction f as [|a f IHf].
   - compute.
     tauto.
   - rewrite make_conj_cons.
@@ -489,10 +490,10 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
 
 Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t.
 Proof.
-  intros.
+  intros T env t tg.
   rewrite <- xnnormalise_correct.
   unfold normalise.
-  generalize (xnnormalise t) as f;intro.
+  generalize (xnnormalise t) as f;intro f.
   destruct (Zunsat f) eqn:U.
   - assert (US := Zunsat_sound _  U env).
     rewrite eval_cnf_ff.
@@ -519,10 +520,10 @@ Definition negate {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
 Lemma xnegate_correct : forall env f,
     (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f.
 Proof.
-  intros.
+  intros env f.
   destruct f as [e o]; destruct o eqn:Op; cbn - [psub];
     repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc;
-      generalize (eval_pol env e) as x; intro.
+      generalize (eval_pol env e) as x; intro x.
   - tauto.
   - rewrite eq_cnf.
     destruct (Z.eq_decidable x 0);tauto.
@@ -533,10 +534,10 @@ Qed.
 
 Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t.
 Proof.
-  intros.
+  intros T env t tg.
   rewrite <- xnnormalise_correct.
   unfold negate.
-  generalize (xnnormalise t) as f;intro.
+  generalize (xnnormalise t) as f;intro f.
   destruct (Zunsat f) eqn:U.
   - assert (US := Zunsat_sound _  U env).
     rewrite eval_cnf_tt.
@@ -569,10 +570,10 @@ Require Import Znumtheory.
 Lemma Zdivide_ceiling : forall a b, (b | a) -> ceiling a b = Z.div a b.
 Proof.
   unfold ceiling.
-  intros.
+  intros a b H.
   apply Zdivide_mod in H.
   case_eq (Z.div_eucl a b).
-  intros.
+  intros z z0 H0.
   change z with (fst (z,z0)).
   rewrite <- H0.
   change (fst (Z.div_eucl a b)) with (Z.div a b).
@@ -642,12 +643,12 @@ Definition isZ0 (x:Z) :=
 
 Lemma isZ0_0 : forall x, isZ0 x = true <-> x = 0.
 Proof.
-  destruct x ; simpl ; intuition congruence.
+  intros x; destruct x ; simpl ; intuition congruence.
 Qed.
 
 Lemma isZ0_n0 : forall x, isZ0 x = false <-> x <> 0.
 Proof.
-  destruct x ; simpl ; intuition congruence.
+  intros x; destruct x ; simpl ; intuition congruence.
 Qed.
 
 Definition ZgcdM (x y : Z) := Z.max (Z.gcd x y) 1.
@@ -682,8 +683,8 @@ Inductive Zdivide_pol (x:Z): PolC Z -> Prop :=
 Lemma Zdiv_pol_correct : forall a p, 0 < a -> Zdivide_pol a p  ->
   forall env, eval_pol env p =  a * eval_pol env (Zdiv_pol p a).
 Proof.
-  intros until 2.
-  induction H0.
+  intros a p H H0.
+  induction H0 as [? ?|? ? IHZdivide_pol j|? ? ? IHZdivide_pol1 ? IHZdivide_pol2 j].
   (* Pc *)
   simpl.
   intros.
@@ -702,7 +703,7 @@ Qed.
 
 Lemma Zgcd_pol_ge : forall p, fst (Zgcd_pol p) >= 0.
 Proof.
-  induction p. 1-2: easy.
+  intros p; induction p as [c|p p1 IHp1|p1 IHp1 ? p3 IHp3]. 1-2: easy.
   simpl.
   case_eq (Zgcd_pol p1).
   case_eq (Zgcd_pol p3).
@@ -715,7 +716,7 @@ Qed.
 
 Lemma Zdivide_pol_Zdivide : forall p x y, Zdivide_pol x p -> (y | x) ->  Zdivide_pol y p.
 Proof.
-  intros.
+  intros p x y H H0.
   induction H.
   constructor.
   apply Z.divide_trans with (1:= H0) ; assumption.
@@ -725,7 +726,7 @@ Qed.
 
 Lemma Zdivide_pol_one : forall p, Zdivide_pol 1 p.
 Proof.
-  induction p ; constructor ; auto.
+  intros p; induction p as [c| |]; constructor ; auto.
   exists c. ring.
 Qed.
 
@@ -744,19 +745,19 @@ Lemma Zdivide_pol_sub : forall p a b,
   Zdivide_pol a (PsubC Z.sub p b) ->
    Zdivide_pol (Z.gcd a b) p.
 Proof.
-  induction p.
+  intros p; induction p as [c|? p IHp|p ? ? ? IHp2].
   simpl.
-  intros. inversion H0.
+  intros a b H H0. inversion H0.
   constructor.
   apply Zgcd_minus ; auto.
-  intros.
+  intros ? ? H H0.
   constructor.
   simpl in H0. inversion H0 ; subst; clear H0.
   apply IHp ; auto.
-  simpl. intros.
+  simpl. intros a b H H0.
   inv H0.
   constructor.
-  apply Zdivide_pol_Zdivide with (1:= H3).
+  apply Zdivide_pol_Zdivide with (1:= (ltac:(assumption) : Zdivide_pol a p)).
   destruct (Zgcd_is_gcd a b) ; assumption.
   apply IHp2 ; assumption.
 Qed.
@@ -765,15 +766,15 @@ Lemma Zdivide_pol_sub_0 : forall p a,
   Zdivide_pol a (PsubC Z.sub p 0) ->
    Zdivide_pol a p.
 Proof.
-  induction p.
+  intros p; induction p as [c|? p IHp|? IHp1 ? ? IHp2].
   simpl.
-  intros. inversion H.
+  intros ? H. inversion H.
   constructor. rewrite Z.sub_0_r in *. assumption.
-  intros.
+  intros ? H.
   constructor.
   simpl in H. inversion H ; subst; clear H.
   apply IHp ; auto.
-  simpl. intros.
+  simpl. intros ? H.
   inv H.
   constructor. auto.
   apply IHp2 ; assumption.
@@ -783,9 +784,9 @@ Qed.
 Lemma Zgcd_pol_div : forall p g c,
   Zgcd_pol p = (g, c) -> Zdivide_pol g (PsubC Z.sub p c).
 Proof.
-  induction p ; simpl.
+  intros p; induction p as [c|? ? IHp|p1 IHp1 ? p3 IHp2]; simpl.
   (* Pc *)
-  intros. inv H.
+  intros ? ? H. inv H.
   constructor.
   exists 0. now ring.
   (* Pinj *)
@@ -793,28 +794,28 @@ Proof.
   constructor.  apply IHp ; auto.
   (* PX *)
   intros g c.
-  case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros.
+  case_eq (Zgcd_pol p1) ; case_eq (Zgcd_pol p3) ; intros z z0 H z1 z2 H0 H1.
   inv H1.
   unfold ZgcdM at 1.
   destruct (Zmax_spec (Z.gcd (ZgcdM z1 z2) z) 1) as [HH1 | HH1];
   destruct HH1 as [HH1 HH1'] ; rewrite HH1'.
   constructor.
-  apply Zdivide_pol_Zdivide with (x:= ZgcdM z1 z2).
+  apply (Zdivide_pol_Zdivide _ (ZgcdM z1 z2)).
   unfold ZgcdM.
   destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
-  destruct HH2.
+  destruct HH2 as [H1 H2].
   rewrite H2.
   apply Zdivide_pol_sub ; auto.
   apply Z.lt_le_trans with 1. reflexivity. now apply Z.ge_le.
-  destruct HH2. rewrite H2.
+  destruct HH2 as [H1 H2]. rewrite H2.
   apply Zdivide_pol_one.
   unfold ZgcdM in HH1. unfold ZgcdM.
   destruct (Zmax_spec  (Z.gcd z1 z2)  1) as [HH2 | HH2].
-  destruct HH2. rewrite H2 in *.
+  destruct HH2 as [H1 H2]. rewrite H2 in *.
   destruct (Zgcd_is_gcd (Z.gcd z1 z2) z); auto.
-  destruct HH2. rewrite H2.
+  destruct HH2 as [H1 H2]. rewrite H2.
   destruct (Zgcd_is_gcd 1  z); auto.
-  apply Zdivide_pol_Zdivide with (x:= z).
+  apply (Zdivide_pol_Zdivide _ z).
   apply (IHp2 _ _ H); auto.
   destruct (Zgcd_is_gcd (ZgcdM z1 z2) z); auto.
   constructor. apply Zdivide_pol_one.
@@ -873,7 +874,7 @@ Definition is_pol_Z0 (p : PolC Z) : bool :=
 Lemma is_pol_Z0_eval_pol : forall p, is_pol_Z0 p = true -> forall env, eval_pol env p = 0.
 Proof.
   unfold is_pol_Z0.
-  destruct p ; try discriminate.
+  intros p; destruct p as [z| |]; try discriminate.
   destruct z ; try discriminate.
   reflexivity.
 Qed.
@@ -915,8 +916,8 @@ Fixpoint max_var (jmp : positive) (p : Pol Z) : positive :=
 Lemma pos_le_add : forall y x,
     (x <= y + x)%positive.
 Proof.
-  intros.
-  assert  ((Z.pos x) <= Z.pos (x + y))%Z.
+  intros y x.
+  assert  ((Z.pos x) <= Z.pos (x + y))%Z as H.
   rewrite <- (Z.add_0_r (Zpos x)).
   rewrite <- Pos2Z.add_pos_pos.
   apply Z.add_le_mono_l.
@@ -929,10 +930,10 @@ Qed.
 Lemma max_var_le : forall p v,
     (v <= max_var v p)%positive.
 Proof.
-  induction p; simpl.
+  intros p; induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl.
   - intros.
     apply Pos.le_refl.
-  - intros.
+  - intros v.
     specialize (IHp (p+v)%positive).
     eapply Pos.le_trans ; eauto.
     assert (xH + v <= p + v)%positive.
@@ -942,7 +943,7 @@ Proof.
     }
     eapply Pos.le_trans ; eauto.
     apply pos_le_add.
-  - intros.
+  - intros v.
     apply Pos.max_case_strong;intros ; auto.
     specialize (IHp2 (Pos.succ v)%positive).
     eapply Pos.le_trans ; eauto.
@@ -951,10 +952,10 @@ Qed.
 Lemma max_var_correct : forall p j v,
     In v (vars j p) -> Pos.le v (max_var j p).
 Proof.
-  induction p; simpl.
+  intros p; induction p; simpl.
   - tauto.
   - auto.
-  - intros.
+  - intros j v H.
     rewrite in_app_iff in H.
     destruct H as [H |[ H | H]].
     + subst.
@@ -980,7 +981,7 @@ Section MaxVar.
       (v <= acc ->
        v <= fold_left F l acc)%positive.
   Proof.
-    induction l ; simpl ; [easy|].
+    intros l; induction l as [|a l IHl] ; simpl ; [easy|].
     intros.
     apply IHl.
     unfold F.
@@ -993,7 +994,7 @@ Section MaxVar.
       (acc <= acc' ->
        fold_left F l acc <= fold_left F l acc')%positive.
   Proof.
-    induction l ; simpl ; [easy|].
+    intros l; induction l as [|a l IHl]; simpl ; [easy|].
     intros.
     apply IHl.
     unfold F.
@@ -1006,13 +1007,13 @@ Section MaxVar.
   Lemma max_var_nformulae_correct_aux : forall l p o v,
       In (p,o) l -> In v (vars xH p) -> Pos.le v (fold_left F l 1)%positive.
   Proof.
-  intros.
+  intros l p o v H H0.
   generalize 1%positive as acc.
   revert p o v H H0.
-  induction l.
+  induction l as [|a l IHl].
   - simpl. tauto.
   - simpl.
-    intros.
+    intros p o v H H0 ?.
     destruct H ; subst.
     + unfold F at 2.
       simpl.
@@ -1128,14 +1129,14 @@ Require Import Wf_nat.
 
 Lemma in_bdepth : forall l a b  y, In y l ->  ltof ZArithProof bdepth y (EnumProof a b  l).
 Proof.
-  induction l.
+  intros l; induction l as [|a l IHl].
   (* nil *)
   simpl.
   tauto.
   (* cons *)
   simpl.
-  intros.
-  destruct H.
+  intros a0 b y H.
+  destruct H as [H|H].
   subst.
   unfold ltof.
   simpl.
@@ -1180,8 +1181,8 @@ Lemma eval_Psatz_sound : forall env w l f',
   make_conj (eval_nformula env) l ->
   eval_Psatz l w  = Some f' ->  eval_nformula env f'.
 Proof.
-  intros.
-  apply (eval_Psatz_Sound Zsor ZSORaddon) with (l:=l) (e:= w) ; auto.
+  intros env w l f' H H0.
+  apply (fun H => eval_Psatz_Sound Zsor ZSORaddon l _ H w) ; auto.
   apply make_conj_in ; auto.
 Qed.
 
@@ -1193,7 +1194,7 @@ Proof.
   unfold nformula_of_cutting_plane.
   unfold eval_nformula. unfold RingMicromega.eval_nformula.
   unfold eval_op1.
-  intros.
+  intros env e e' c H H0.
   rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
   simpl.
   (**)
@@ -1201,10 +1202,10 @@ Proof.
   revert H0.
   case_eq (Zgcd_pol e) ; intros g c0.
   generalize (Zgt_cases g 0) ; destruct (Z.gtb g 0).
-  intros.
+  intros H0 H1 H2.
   inv H2.
   change (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x)) with eval_pol in *.
-  apply Zgcd_pol_correct_lt with (env:=env) in H1. 2: auto using Z.gt_lt.
+  apply (Zgcd_pol_correct_lt _ env) in H1. 2: auto using Z.gt_lt.
   apply Z.le_add_le_sub_l, Z.ge_le; rewrite Z.add_0_r.
   apply (narrow_interval_lower_bound g (- c0) (eval_pol env (Zdiv_pol (PsubC Z.sub e c0) g)) H0).
   apply Z.le_ge.
@@ -1213,7 +1214,7 @@ Proof.
   rewrite <- H1.
   assumption.
   (* g <= 0 *)
-  intros. inv H2. auto with zarith.
+  intros H0 H1 H2. inv H2. auto with zarith.
 Qed.
 
 Lemma cutting_plane_sound : forall env f p,
@@ -1222,34 +1223,34 @@ Lemma cutting_plane_sound : forall env f p,
    eval_nformula env (nformula_of_cutting_plane p).
 Proof.
   unfold genCuttingPlane.
-  destruct f as [e op].
+  intros env f; destruct f as [e op].
   destruct op.
   (* Equal *)
-  destruct p as [[e' z] op].
+  intros p; destruct p as [[e' z] op].
   case_eq (Zgcd_pol e) ; intros g c.
   case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))) ; [discriminate|].
   case_eq (makeCuttingPlane e).
-  intros.
+  intros ? ? H H0 H1 H2 H3.
   inv H3.
   unfold makeCuttingPlane in H.
   rewrite H1 in H.
   revert H.
   change (eval_pol env e = 0) in H2.
   case_eq (Z.gtb g 0).
-  intros.
-  rewrite <- Zgt_is_gt_bool in H.  
+  intros H H3.
+  rewrite <- Zgt_is_gt_bool in H.
   rewrite Zgcd_pol_correct_lt with (1:= H1)  in H2. 2: auto using Z.gt_lt.
-  unfold nformula_of_cutting_plane.  
+  unfold nformula_of_cutting_plane.
   change (eval_pol env (padd e' (Pc z)) = 0).
   inv H3.
   rewrite eval_pol_add.
   set (x:=eval_pol env (Zdiv_pol (PsubC Z.sub e c) g)) in *; clearbody x.
   simpl.
   rewrite andb_false_iff in H0.
-  destruct H0.
+  destruct H0 as [H0|H0].
   rewrite Zgt_is_gt_bool in H ; congruence.
   rewrite andb_false_iff in H0.
-  destruct H0.
+  destruct H0 as [H0|H0].
   rewrite negb_false_iff in H0.
   apply Zeq_bool_eq in H0.
   subst. simpl.
@@ -1259,13 +1260,13 @@ Proof.
   apply Zeq_bool_eq in H0.
   assert (HH := Zgcd_is_gcd g c).
   rewrite H0 in HH.
-  inv HH.
+  destruct HH as [H3 H4 ?].
   apply Zdivide_opp_r in H4.
   rewrite Zdivide_ceiling ; auto.
   apply Z.sub_move_0_r.
   apply Z.div_unique_exact. now intros ->.
   now rewrite Z.add_move_0_r in H2.
-  intros.
+  intros H H3.
   unfold nformula_of_cutting_plane.
   inv H3.
   change (eval_pol env (padd e' (Pc 0)) = 0).
@@ -1273,7 +1274,7 @@ Proof.
   simpl.
   now rewrite Z.add_0_r.
   (* NonEqual *)
-  intros.
+  intros ? H H0.
   inv H0.
   unfold eval_nformula in *.
   unfold RingMicromega.eval_nformula in *.
@@ -1282,20 +1283,20 @@ Proof.
   rewrite (RingMicromega.eval_pol_add Zsor ZSORaddon).
   simpl. now rewrite Z.add_0_r.
   (* Strict *)
-  destruct p as [[e' z] op].
+  intros p; destruct p as [[e' z] op].
   case_eq (makeCuttingPlane (PsubC Z.sub e 1)).
-  intros.
+  intros ? ? H H0 H1.
   inv H1.
-  apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
+  apply (makeCuttingPlane_ns_sound env) with (2:= H).
   simpl in *.
   rewrite (RingMicromega.PsubC_ok Zsor ZSORaddon).
   now apply Z.lt_le_pred.
   (* NonStrict *)
-  destruct p as [[e' z] op].
+  intros p; destruct p as [[e' z] op].
   case_eq (makeCuttingPlane e).
-  intros.
+  intros ? ? H H0 H1.
   inv H1.
-  apply makeCuttingPlane_ns_sound with (env:=env) (2:= H).
+  apply (makeCuttingPlane_ns_sound env) with (2:= H).
   assumption.
 Qed.
 
@@ -1304,12 +1305,15 @@ Lemma  genCuttingPlaneNone : forall env f,
   eval_nformula env f -> False.
 Proof.
   unfold genCuttingPlane.
-  destruct f.
+  intros env f; destruct f as [p o].
   destruct o.
   case_eq (Zgcd_pol p) ; intros g c.
   case_eq (Z.gtb g 0 && (negb (Zeq_bool c 0) && negb (Zeq_bool (Z.gcd g c) g))).
-  intros.
+  intros H H0 H1 H2.
   flatten_bool.
+  match goal with [ H' : (g >? 0) = true |- ?G ] => rename H' into H3 end.
+  match goal with [ H' : negb (Zeq_bool c 0) = true |- ?G ] => rename H' into H end.
+  match goal with [ H' : negb (Zeq_bool (Z.gcd g c) g) = true |- ?G ] => rename H' into H5 end.
   rewrite negb_true_iff in H5.
   apply Zeq_bool_neq in H5.
   rewrite <- Zgt_is_gt_bool in H3.
@@ -1359,7 +1363,7 @@ Lemma agree_env_subset : forall v1 v2 env env',
     agree_env v2 env env'.
 Proof.
   unfold agree_env.
-  intros.
+  intros v1 v2 env env' H ? ? ?.
   apply H.
   eapply Pos.le_trans ; eauto.
 Qed.
@@ -1369,7 +1373,7 @@ Lemma agree_env_jump : forall fr j env env',
     agree_env (fr + j) env env' ->
     agree_env fr (Env.jump j env) (Env.jump j env').
 Proof.
-  intros.
+  intros fr j env env' H.
   unfold agree_env ; intro.
   intros.
   unfold Env.jump.
@@ -1382,7 +1386,7 @@ Lemma agree_env_tail : forall fr env env',
     agree_env (Pos.succ fr) env env' ->
     agree_env fr (Env.tail env) (Env.tail env').
 Proof.
-  intros.
+  intros fr env env' H.
   unfold Env.tail.
   apply agree_env_jump.
   rewrite <- Pos.add_1_r in H.
@@ -1393,7 +1397,7 @@ Qed.
 Lemma max_var_acc : forall p i j,
     (max_var (i + j) p = max_var i p + j)%positive.
 Proof.
-  induction p; simpl.
+  intros p; induction p as [|? ? IHp|? IHp1 ? ? IHp2]; simpl.
   - reflexivity.
   - intros.
     rewrite ! IHp.
@@ -1415,27 +1419,27 @@ Lemma agree_env_eval_nformula :
          (AGREE : agree_env (max_var xH (fst e))  env env'),
     eval_nformula env e  <->  eval_nformula env' e.
 Proof.
-  destruct e.
-  simpl; intros.
+  intros env env' e; destruct e as [p o].
+  simpl; intros AGREE.
   assert ((RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env p)
           =
-          (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)).
+          (RingMicromega.eval_pol Z.add Z.mul (fun x : Z => x) env' p)) as H.
   {
     revert env env' AGREE.
     generalize xH.
-    induction p ; simpl.
+    induction p as [?|p ? IHp|? IHp1 ? ? IHp2]; simpl.
     - reflexivity.
-    - intros.
-      apply IHp with (p := p1%positive).
+    - intros p1 **.
+      apply (IHp p1).
       apply agree_env_jump.
       eapply agree_env_subset; eauto.
       rewrite (Pos.add_comm p).
       rewrite max_var_acc.
       apply Pos.le_refl.
-    - intros.
+    - intros p ? ? AGREE.
       f_equal.
       f_equal.
-      { apply IHp1 with (p:= p).
+      { apply (IHp1 p).
         eapply agree_env_subset; eauto.
         apply Pos.le_max_l.
       }
@@ -1446,7 +1450,7 @@ Proof.
         apply Pos.le_1_l.
       }
       {
-        apply IHp2 with (p := p).
+        apply (IHp2 p).
         apply agree_env_tail.
         eapply agree_env_subset; eauto.
         rewrite !Pplus_one_succ_r.
@@ -1463,11 +1467,11 @@ Lemma agree_env_eval_nformulae :
          make_conj (eval_nformula env) l <->
          make_conj (eval_nformula env') l.
 Proof.
-  induction l.
+  intros env env' l; induction l as [|a l IHl].
   - simpl. tauto.
   - intros.
     rewrite ! make_conj_cons.
-    assert (eval_nformula env a <-> eval_nformula env' a).
+    assert (eval_nformula env a <-> eval_nformula env' a) as H.
     {
       apply agree_env_eval_nformula.
       eapply agree_env_subset ; eauto.
@@ -1491,7 +1495,7 @@ Qed.
 Lemma eq_true_iff_eq :
   forall b1 b2 : bool, (b1 = true <-> b2 = true) <-> b1 = b2.
 Proof.
-  destruct b1,b2 ; intuition congruence.
+  intros b1 b2; destruct b1,b2 ; intuition congruence.
 Qed.
 
 Ltac pos_tac :=
@@ -1520,7 +1524,7 @@ Qed.
 Lemma ZChecker_sound : forall w l,
     ZChecker l w = true -> forall env, make_impl  (eval_nformula env)  l False.
 Proof.
-  induction w    using (well_founded_ind (well_founded_ltof _ bdepth)).
+  intros w; induction w as [w H] using (well_founded_ind (well_founded_ltof _ bdepth)).
   destruct w as [ | w pf | w pf | p pf1 pf2 | w1 w2 pf | x pf].
   - (* DoneProof *)
   simpl. discriminate.
@@ -1529,12 +1533,12 @@ Proof.
   intros l. case_eq (eval_Psatz l w) ; [| discriminate].
   intros f Hf.
   case_eq (Zunsat f).
-  intros.
+  intros H0 ? ?.
   apply (checker_nf_sound Zsor ZSORaddon l w).
   unfold check_normalised_formulas.  unfold eval_Psatz in Hf. rewrite Hf.
   unfold Zunsat in H0. assumption.
-  intros.
-  assert (make_impl  (eval_nformula env) (f::l) False).
+  intros H0 H1 env.
+  assert (make_impl  (eval_nformula env) (f::l) False) as H2.
    apply H with (2:= H1).
    unfold ltof.
    simpl.
@@ -1553,8 +1557,8 @@ Proof.
   case_eq (eval_Psatz l w) ; [ | discriminate].
   intros f' Hlc.
   case_eq (genCuttingPlane f').
-  intros.
-  assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False).
+  intros p H0 H1 env.
+  assert (make_impl (eval_nformula env) (nformula_of_cutting_plane p::l) False) as H2.
    eapply (H pf)  ; auto.
    unfold ltof.
    simpl.
@@ -1565,13 +1569,13 @@ Proof.
   intro.
   apply H2.
   split ; auto.
-  apply eval_Psatz_sound with (env:=env) in Hlc.
+  apply (eval_Psatz_sound env) in Hlc.
   apply cutting_plane_sound with (1:= Hlc) (2:= H0).
   auto.
   (* genCuttingPlane = None *)
-  intros.
+  intros H0 H1 env.
   rewrite <- make_conj_impl.
-  intros.
+  intros H2.
   apply eval_Psatz_sound with (2:= Hlc) in H2.
   apply genCuttingPlaneNone with (2:= H2) ; auto.
   - (* SplitProof *)
@@ -1581,18 +1585,20 @@ Proof.
     case_eq (genCuttingPlane (popp p, NonStrict)) ; [| discriminate].
     intros cp1 GCP1 cp2 GCP2 ZC1 env.
     flatten_bool.
+    match goal with [ H' : ZChecker _ pf1 = true |- _ ] => rename H' into H0 end.
+    match goal with [ H' : ZChecker _ pf2 = true |- _ ] => rename H' into H1 end.
     destruct (eval_nformula_split env p).
-    + apply H with (env:=env) in H0.
+    + apply (fun H' ck => H _ H' _ ck env) in H0.
       rewrite <- make_conj_impl in *.
       intro ; apply H0.
       rewrite make_conj_cons. split; auto.
-      apply cutting_plane_sound with (f:= (p,NonStrict)) ; auto.
+      apply (cutting_plane_sound _ (p,NonStrict)) ; auto.
       apply ltof_bdepth_split_l.
-    + apply H with (env:=env) in H1.
+    + apply (fun H' ck => H _ H' _ ck env) in H1.
       rewrite <- make_conj_impl in *.
       intro ; apply H1.
       rewrite make_conj_cons. split; auto.
-      apply cutting_plane_sound with (f:= (popp p,NonStrict)) ; auto.
+      apply (cutting_plane_sound _ (popp p,NonStrict)) ; auto.
       apply ltof_bdepth_split_r.
   - (* EnumProof *)
   intros l.
@@ -1601,22 +1607,22 @@ Proof.
   case_eq (eval_Psatz l w2) ; [  | discriminate].
   intros f1 Hf1 f2 Hf2.
   case_eq (genCuttingPlane f2).
-  destruct p as [ [p1 z1] op1].
+  intros p; destruct p as [ [p1 z1] op1].
   case_eq (genCuttingPlane f1).
-  destruct p as [ [p2 z2] op2].
+  intros p; destruct p as [ [p2 z2] op2].
   case_eq (valid_cut_sign op1 && valid_cut_sign op2 && is_pol_Z0 (padd p1 p2)).
   intros Hcond.
   flatten_bool.
-  rename H1 into HZ0.
-  rename H2 into Hop1.
-  rename H3 into Hop2.
+  match goal with [ H1 : is_pol_Z0 (padd p1 p2) = true |- _ ] => rename H1 into HZ0 end.
+  match goal with [ H2 : valid_cut_sign op1 = true |- _ ] => rename H2 into Hop1 end.
+  match goal with [ H3 : valid_cut_sign op2 = true |- _ ] => rename H3 into Hop2 end.
   intros HCutL HCutR Hfix env.
   (* get the bounds of the enum *)
   rewrite <- make_conj_impl.
-  intro.
-  assert (-z1 <= eval_pol env p1 <= z2).
+  intro H0.
+  assert (-z1 <= eval_pol env p1 <= z2) as H1.
    split.
-   apply  eval_Psatz_sound with (env:=env) in Hf2 ; auto.
+   apply  (eval_Psatz_sound env) in Hf2 ; auto.
    apply cutting_plane_sound with (1:= Hf2) in HCutR.
    unfold nformula_of_cutting_plane in HCutR.
    unfold eval_nformula in HCutR.
@@ -1628,10 +1634,10 @@ Proof.
      rewrite Z.add_move_0_l in HCutR; rewrite HCutR, Z.opp_involutive; reflexivity.
      now apply Z.le_sub_le_add_r in HCutR.
    (**)
-   apply is_pol_Z0_eval_pol with (env := env) in HZ0.
+   apply (fun H => is_pol_Z0_eval_pol _ H env) in HZ0.
    rewrite eval_pol_add, Z.add_move_r, Z.sub_0_l in HZ0.
    rewrite HZ0.
-   apply  eval_Psatz_sound with (env:=env) in Hf1 ; auto.
+   apply  (eval_Psatz_sound env) in Hf1 ; auto.
    apply cutting_plane_sound with (1:= Hf1) in HCutL.
    unfold nformula_of_cutting_plane in HCutL.
    unfold eval_nformula in HCutL.
@@ -1647,7 +1653,7 @@ Proof.
   match goal with
     | |- context[?F pf (-z1) z2 = true] => set (FF := F)
   end.
-  intros.
+  intros Hfix.
   assert (HH :forall x, -z1 <= x <= z2 -> exists pr,
     (In pr pf /\
       ZChecker ((PsubC Z.sub p1 x,Equal) :: l) pr = true)%Z).
@@ -1655,16 +1661,18 @@ Proof.
   revert Hfix.
   generalize (-z1). clear z1. intro z1.
   revert z1 z2.
-  induction pf;simpl ;intros.
+  induction pf as [|a pf IHpf];simpl ;intros z1 z2 Hfix x **.
   revert Hfix.
   now case (Z.gtb_spec); [ | easy ]; intros LT; elim (Zlt_not_le _ _ LT); transitivity x.
   flatten_bool.
+  match goal with [ H' : _ <= x <= _ |- _ ] => rename H' into H0 end.
+  match goal with [ H' : FF pf (z1 + 1) z2 = true |- _ ] => rename H' into H2 end.
   destruct (Z_le_lt_eq_dec _ _ (proj1 H0)) as [ LT | -> ].
   2: exists a; auto.
   rewrite <- Z.le_succ_l in LT.
   assert (LE: (Z.succ z1 <= x <= z2)%Z) by intuition.
   elim IHpf with (2:=H2) (3:= LE).
-  intros.
+  intros x0 ?.
   exists x0 ; split;tauto.
   intros until 1. 
   apply H ; auto. 
@@ -1676,7 +1684,7 @@ Proof.
   apply Z.add_le_mono_r. assumption.
   (*/asser *)
   destruct (HH _ H1) as [pr [Hin Hcheker]].
-  assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False).
+  assert (make_impl (eval_nformula env) ((PsubC Z.sub p1 (eval_pol env p1),Equal) :: l) False) as H2.
    eapply (H pr)  ;auto.
    apply in_bdepth ; auto.
   rewrite <- make_conj_impl in H2.
@@ -1690,15 +1698,15 @@ Proof.
   unfold eval_pol. ring.
   discriminate.
   (* No cutting plane *)
-  intros.
+  intros H0 H1 H2 env.
   rewrite <- make_conj_impl.
-  intros.
+  intros H3.
   apply eval_Psatz_sound with (2:= Hf1) in H3.
   apply genCuttingPlaneNone with (2:= H3) ; auto.
   (* No Cutting plane (bis) *)
-  intros.
+  intros H0 H1 env.
   rewrite <- make_conj_impl.
-  intros.
+  intros H2.
   apply eval_Psatz_sound with (2:= Hf2) in H2.
   apply genCuttingPlaneNone with (2:= H2) ; auto.
 - intros l.
@@ -1708,15 +1716,15 @@ Proof.
   set (z1 := (Pos.succ fr)) in *.
   set (t1 := (Pos.succ z1)) in *.
   destruct (x <=? fr)%positive eqn:LE ; [|congruence].
-  intros.
+  intros H0 env.
   set (env':= fun v => if Pos.eqb v z1
                        then if Z.leb (env x) 0 then 0 else env x
                        else if Pos.eqb v t1
                             then if Z.leb (env x) 0 then -(env x) else 0
                             else env v).
-  apply H with (env:=env') in H0.
+  apply (fun H' ck => H _ H' _ ck env') in H0.
   + rewrite <- make_conj_impl in *.
-    intro.
+    intro H1.
     rewrite !make_conj_cons in H0.
     apply H0 ; repeat split.
     *
@@ -1729,17 +1737,17 @@ Proof.
       destruct (env x <=? 0); ring.
       { unfold t1.
         pos_tac; normZ.
-        lia (Hyp H2).
+        lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)).
       }
       {
         unfold t1, z1.
         pos_tac; normZ.
-        lia (Add (Hyp LE) (Hyp H3)).
+        lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.succ (Z.pos fr))) ltac:(assumption))).
       }
       {
         unfold z1.
         pos_tac; normZ.
-        lia (Add (Hyp LE) (Hyp H3)).
+        lia (Add (Hyp LE) (Hyp (e := Z.pos x - Z.succ (Z.pos fr)) ltac:(assumption))).
       }
     *
       apply eval_nformula_bound_var.
@@ -1749,7 +1757,7 @@ Proof.
       compute. congruence.
       rewrite Z.leb_gt in EQ.
       normZ.
-      lia (Add (Hyp EQ) (Hyp H2)).
+      lia (Add (Hyp EQ) (Hyp (e := 0 - (env x + 1)) ltac:(assumption))).
     *
       apply eval_nformula_bound_var.
       unfold env'.
@@ -1758,15 +1766,15 @@ Proof.
       destruct (env x <=? 0) eqn:EQ.
       rewrite Z.leb_le in EQ.
       normZ.
-      lia (Add (Hyp EQ) (Hyp H2)).
+      lia (Add (Hyp EQ) (Hyp (e := 0 - (- env x + 1)) ltac:(assumption))).
       compute; congruence.
       unfold t1.
       clear.
       pos_tac; normZ.
-      lia (Hyp H).
+      lia (Hyp (e := Z.pos z1 - Z.succ (Z.pos z1)) ltac:(assumption)).
     *
-      rewrite agree_env_eval_nformulae with (env':= env') in H1;auto.
-      unfold agree_env; intros.
+      rewrite (agree_env_eval_nformulae _ env') in H1;auto.
+      unfold agree_env; intros x0 H2.
       unfold env'.
       replace (x0 =? z1)%positive with false.
       replace (x0 =? t1)%positive with false.
@@ -1776,13 +1784,13 @@ Proof.
         unfold fr in *.
         apply Pos2Z.pos_le_pos in H2.
         pos_tac; normZ.
-        lia (Add (Hyp H2) (Hyp H4)).
+        lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.succ (Z.pos (max_var_nformulae l)))) ltac:(assumption))).
       }
       {
         unfold z1, fr in *.
         apply Pos2Z.pos_le_pos in H2.
         pos_tac; normZ.
-        lia (Add (Hyp H2) (Hyp H4)).
+        lia (Add (Hyp H2) (Hyp (e := Z.pos x0 - Z.succ (Z.pos (max_var_nformulae l))) ltac:(assumption))).
       }
   + unfold ltof.
     simpl.
@@ -1796,27 +1804,27 @@ Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env,
 Proof.
   intros f w.
   unfold ZTautoChecker.
-  apply tauto_checker_sound with (eval' := eval_nformula).
+  apply (tauto_checker_sound _ _ _ _ eval_nformula).
   - apply Zeval_nformula_dec.
-  - intros until env.
+  - intros t ? env.
   unfold eval_nformula. unfold RingMicromega.eval_nformula.
   destruct t.
   apply (check_inconsistent_sound Zsor ZSORaddon) ; auto.
-  - unfold Zdeduce. intros. revert H.
+  - unfold Zdeduce. intros ? ? ? H **. revert H.
      apply (nformula_plus_nformula_correct Zsor ZSORaddon); auto.
   -
-    intros.
+    intros ? ? ? ? H.
     rewrite normalise_correct  in H.
     rewrite Zeval_formula_compat; auto.
   -
-    intros.
+    intros ? ? ? ? H.
     rewrite negate_correct in H ; auto.
     rewrite Tauto.hold_eNOT.
     rewrite Zeval_formula_compat; auto.
   - intros t w0.
     unfold eval_tt.
-    intros.
-    rewrite make_impl_map with (eval := eval_nformula env).
+    intros H env.
+    rewrite (make_impl_map (eval_nformula env)).
     eapply ZChecker_sound; eauto.
     tauto.
 Qed.
diff --git a/theories/setoid_ring/Field_theory.v b/theories/setoid_ring/Field_theory.v
index c12f46bed6..4b3bba9843 100644
--- a/theories/setoid_ring/Field_theory.v
+++ b/theories/setoid_ring/Field_theory.v
@@ -397,7 +397,7 @@ Qed.
 Theorem cross_product_eq a b c d :
   ~ b == 0 -> ~ d == 0 -> a * d == c * b -> a / b == c / d.
 Proof.
-intros.
+intros H H0 H1.
 transitivity (a / b * (d / d)).
 - now rewrite rdiv_r_r, rmul_1_r.
 - now rewrite rdiv4, H1, (rmul_comm b d), <- rdiv4, rdiv_r_r.
@@ -418,23 +418,23 @@ Qed.
 
 Lemma pow_pos_0 p : pow_pos rmul 0 p == 0.
 Proof.
-induction p;simpl;trivial; now rewrite !IHp.
+induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !IHp.
 Qed.
 
 Lemma pow_pos_1 p : pow_pos rmul 1 p == 1.
 Proof.
-induction p;simpl;trivial; ring [IHp].
+induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp].
 Qed.
 
 Lemma pow_pos_cst c p : pow_pos rmul [c] p == [pow_pos cmul c p].
 Proof.
-induction p;simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp.
+induction p as [p IHp|p IHp|];simpl;trivial; now rewrite !(morph_mul CRmorph), !IHp.
 Qed.
 
 Lemma pow_pos_mul_l x y p :
  pow_pos rmul (x * y) p == pow_pos rmul x p * pow_pos rmul y p.
 Proof.
-induction p;simpl;trivial; ring [IHp].
+induction p as [p IHp|p IHp|];simpl;trivial; ring [IHp].
 Qed.
 
 Lemma pow_pos_add_r x p1 p2 :
@@ -446,7 +446,7 @@ Qed.
 Lemma pow_pos_mul_r x p1 p2 :
   pow_pos rmul x (p1*p2) == pow_pos rmul (pow_pos rmul x p1) p2.
 Proof.
-induction p1;simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r;
+induction p1 as [p1 IHp1|p1 IHp1|];simpl;intros; rewrite ?pow_pos_mul_l, ?pow_pos_add_r;
  simpl; trivial; ring [IHp1].
 Qed.
 
@@ -459,8 +459,8 @@ Qed.
 Lemma pow_pos_div a b p : ~ b == 0 ->
  pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p.
 Proof.
- intros.
- induction p; simpl; trivial.
+ intros H.
+ induction p as [p IHp|p IHp|]; simpl; trivial.
  - rewrite IHp.
    assert (nz := pow_pos_nz p H).
    rewrite !rdiv4; trivial.
@@ -578,14 +578,15 @@ Qed.
 Theorem PExpr_eq_semi_ok e e' :
  PExpr_eq e e' = true ->  (e === e')%poly.
 Proof.
-revert e'; induction e; destruct e'; simpl; try discriminate.
+revert e'; induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe ?];
+ intro e'; destruct e'; simpl; try discriminate.
 - intros H l. now apply (morph_eq CRmorph).
 - case Pos.eqb_spec; intros; now subst.
 - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
 - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
 - intros H; destruct (if_true _ _ H). now rewrite IHe1, IHe2.
 - intros H. now rewrite IHe.
-- intros H. destruct (if_true _ _ H).
+- intros H. destruct (if_true _ _ H) as [H0 H1].
   apply N.eqb_eq in H0. now rewrite IHe, H0.
 Qed.
 
@@ -667,7 +668,7 @@ Proof.
  - case Pos.eqb_spec; [intro; subst | intros _].
    + simpl. now rewrite rpow_pow.
    + destruct e;simpl;trivial.
-     repeat case ceqb_spec; intros; rewrite ?rpow_pow, ?H; simpl.
+     repeat case ceqb_spec; intros H **; rewrite ?rpow_pow, ?H; simpl.
      * now rewrite phi_1, pow_pos_1.
      * now rewrite phi_0, pow_pos_0.
      * now rewrite pow_pos_cst.
@@ -686,7 +687,8 @@ Infix "**" := NPEmul (at level 40, left associativity).
 Theorem NPEmul_ok e1 e2 : (e1 ** e2 === e1 * e2)%poly.
 Proof.
 intros l.
-revert e2; induction e1;destruct e2; simpl;try reflexivity;
+revert e2; induction e1 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1|? IHe1 n];
+ intro e2; destruct e2; simpl;try reflexivity;
  repeat (case ceqb_spec; intro H; try rewrite H; clear H);
  simpl; try reflexivity; try ring [phi_0 phi_1].
  apply (morph_mul CRmorph).
@@ -801,7 +803,7 @@ Qed.
 Theorem PCond_app l l1 l2 :
  PCond l (l1 ++ l2) <-> PCond l l1 /\ PCond l l2.
 Proof.
-induction l1.
+induction l1 as [|a l1 IHl1].
 - simpl. split; [split|destruct 1]; trivial.
 - simpl app. rewrite !PCond_cons, IHl1. symmetry; apply and_assoc.
 Qed.
@@ -813,7 +815,7 @@ Definition absurd_PCond := cons 0%poly nil.
 Lemma absurd_PCond_bottom : forall l, ~ PCond l absurd_PCond.
 Proof.
 unfold absurd_PCond; simpl.
-red; intros.
+red; intros ? H.
 apply H.
 apply phi_0.
 Qed.
@@ -901,7 +903,7 @@ Theorem isIn_ok e1 p1 e2 p2 :
 Proof.
 Opaque NPEpow.
 revert p1 p2.
-induction e2; intros p1 p2;
+induction e2 as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe2_1 ? IHe2_2|? IHe|? IHe2 n]; intros p1 p2;
  try refine (default_isIn_ok e1 _ p1 p2); simpl isIn.
 - specialize (IHe2_1 p1 p2).
   destruct isIn as [([|p],e)|].
@@ -936,7 +938,7 @@ induction e2; intros p1 p2;
     destruct IHe2_2 as (IH,GT). split; trivial.
     set (d := ZtoN (Z.pos p1 - NtoZ n)) in *; clearbody d.
     npe_simpl. rewrite IH. npe_ring.
-- destruct n; trivial.
+- destruct n as [|p]; trivial.
   specialize (IHe2 p1 (p * p2)%positive).
   destruct isIn as [(n,e)|]; trivial.
   destruct IHe2 as (IH,GT). split; trivial.
@@ -983,7 +985,7 @@ Lemma split_aux_ok1 e1 p e2 :
   /\ e2 === right res * common res)%poly.
 Proof.
  Opaque NPEpow NPEmul.
- intros. unfold res;clear res; generalize (isIn_ok e1 p e2 xH).
+ intros res. unfold res;clear res; generalize (isIn_ok e1 p e2 xH).
  destruct (isIn e1 p e2 1) as [([|p'],e')|]; simpl.
  - intros (H1,H2); split; npe_simpl.
    + now rewrite PE_1_l.
@@ -1000,7 +1002,8 @@ Theorem split_aux_ok: forall e1 p e2,
   (e1 ^ Npos p === left (split_aux e1 p e2) * common (split_aux e1 p e2)
   /\ e2 === right (split_aux e1 p e2) * common (split_aux e1 p e2))%poly.
 Proof.
-induction e1;intros k e2; try refine (split_aux_ok1 _ k e2);simpl.
+intro e1;induction e1 as [| |?|?|? IHe1_1 ? IHe1_2|? IHe1_1 ? IHe1_2|e1_1 IHe1_1 ? IHe1_2|? IHe1|? IHe1 n];
+ intros k e2; try refine (split_aux_ok1 _ k e2);simpl.
 destruct (IHe1_1 k e2) as (H1,H2).
 destruct (IHe1_2 k (right (split_aux e1_1 k e2))) as (H3,H4).
 clear IHe1_1 IHe1_2.
@@ -1101,7 +1104,8 @@ Eval compute
 Theorem Pcond_Fnorm l e :
  PCond l (condition (Fnorm e)) ->  ~ (denum (Fnorm e))@l == 0.
 Proof.
-induction e; simpl condition; rewrite ?PCond_cons, ?PCond_app;
+induction e as [| |?|?|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe1 ? IHe2|? IHe|? IHe|? IHe1 ? IHe2|? IHe n];
+ simpl condition; rewrite ?PCond_cons, ?PCond_app;
  simpl denum; intros (Hc1,Hc2) || intros Hc; rewrite ?NPEmul_ok.
 - simpl. rewrite phi_1; exact rI_neq_rO.
 - simpl. rewrite phi_1; exact rI_neq_rO.
@@ -1141,7 +1145,8 @@ Theorem Fnorm_FEeval_PEeval l fe:
  PCond l (condition (Fnorm fe)) ->
  FEeval l fe == (num (Fnorm fe)) @ l / (denum (Fnorm fe)) @ l.
 Proof.
-induction fe; simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
+induction fe as [| |?|?|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe1 IHfe1 fe2 IHfe2|fe IHfe|fe IHfe|fe1 IHfe1 fe2 IHfe2|fe IHfe n];
+ simpl condition; rewrite ?PCond_cons, ?PCond_app; simpl;
  intros (Hc1,Hc2) || intros Hc;
  try (specialize (IHfe1 Hc1);apply Pcond_Fnorm in Hc1);
  try (specialize (IHfe2 Hc2);apply Pcond_Fnorm in Hc2);
@@ -1260,7 +1265,7 @@ Proof.
   destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
   try ( apply rdiv_ext;
         eapply ring_rw_correct; eauto).
-  destruct (ceqb_spec c cI).
+  destruct (ceqb_spec c cI) as [H0|].
     set (nnum := NPphi_dev _ _).
     apply eq_trans with (nnum / NPphi_dev l (Pc c)).
       apply rdiv_ext;
@@ -1285,7 +1290,7 @@ Proof.
   destruct (Nnorm _ _ _) as [c | | ] eqn: HN;
   try ( apply rdiv_ext;
         eapply ring_rw_pow_correct; eauto).
-  destruct (ceqb_spec c cI).
+  destruct (ceqb_spec c cI) as [H0|].
     set (nnum := NPphi_pow _ _).
     apply eq_trans with (nnum / NPphi_pow l (Pc c)).
       apply rdiv_ext;
@@ -1415,7 +1420,8 @@ Theorem Field_simplify_eq_pow_in_correct :
  NPphi_pow l np1 ==
  NPphi_pow l np2.
 Proof.
- intros. subst nfe1 nfe2 lmp np1 np2.
+ intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?.
+ subst nfe1 nfe2 lmp np1 np2.
  rewrite !(Pphi_pow_ok Rsth Reqe ARth CRmorph pow_th get_sign_spec).
  repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial).
  simpl. apply Field_simplify_aux_ok; trivial.
@@ -1434,7 +1440,8 @@ forall n l lpe fe1 fe2,
  PCond l (condition nfe1 ++ condition nfe2) ->
  NPphi_dev l np1 == NPphi_dev l np2.
 Proof.
- intros. subst nfe1 nfe2 lmp np1 np2.
+ intros n l lpe fe1 fe2 ? lmp ? nfe1 ? nfe2 ? den ? np1 ? np2 ? ? ?.
+ subst nfe1 nfe2 lmp np1 np2.
  rewrite !(Pphi_dev_ok Rsth Reqe ARth CRmorph  get_sign_spec).
  repeat (rewrite <- (norm_subst_ok Rsth Reqe ARth CRmorph pow_th);trivial).
  apply Field_simplify_aux_ok; trivial.
@@ -1458,7 +1465,7 @@ Lemma fcons_ok : forall l l1,
   (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
 Proof.
 intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
-induction l1; simpl; intros.
+induction l1 as [|a l1 IHl1]; simpl; intros.
  trivial.
  elim PCond_fcons_inv with (1 := H); intros.
  destruct l1; trivial. split; trivial. apply IHl1; trivial.
@@ -1480,7 +1487,7 @@ Fixpoint Fcons (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
 Theorem PFcons_fcons_inv:
  forall l a l1, PCond l (Fcons a l1) ->  ~ a @ l == 0 /\ PCond l l1.
 Proof.
-induction l1 as [|e l1]; simpl Fcons.
+intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons.
 - simpl; now split.
 - case PExpr_eq_spec; intros H; rewrite !PCond_cons; intros (H1,H2);
    repeat split; trivial.
@@ -1501,7 +1508,7 @@ Fixpoint Fcons0 (e:PExpr C) (l:list (PExpr C)) {struct l} : list (PExpr C) :=
 Theorem PFcons0_fcons_inv:
  forall l a l1, PCond l (Fcons0 a l1) ->  ~ a @ l == 0 /\ PCond l l1.
 Proof.
-induction l1 as [|e l1]; simpl Fcons0.
+intros l a l1; induction l1 as [|e l1 IHl1]; simpl Fcons0.
 - simpl; now split.
 - generalize (ring_correct O l nil a e). lazy zeta; simpl Peq.
   case Peq; intros H; rewrite !PCond_cons; intros (H1,H2);
@@ -1529,7 +1536,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
   destruct (H0 _ H3) as (H4,H5). split; trivial.
   simpl.
   apply field_is_integral_domain; trivial.
-- intros. destruct (H _ H0). split; trivial.
+- intros ? H ? ? H0. destruct (H _ H0). split; trivial.
   apply PEpow_nz; trivial.
 Qed.
 
@@ -1580,7 +1587,7 @@ intros l a; elim a; try (intros; apply PFcons0_fcons_inv; trivial; fail).
     split; trivial.
     apply ropp_neq_0; trivial.
     rewrite (morph_opp CRmorph), phi_0, phi_1 in H0. trivial.
-- intros. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial.
+- intros ? H ? ? H0. destruct (H _ H0);split;trivial. apply PEpow_nz; trivial.
 Qed.
 
 Definition Fcons2 e l := Fcons1 (PEsimp e) l.
@@ -1674,7 +1681,7 @@ Hypothesis gen_phiPOS_not_0 : forall p, ~ gen_phiPOS1 rI radd rmul p == 0.
 Lemma add_inj_r p x y :
    gen_phiPOS1 rI radd rmul p + x == gen_phiPOS1 rI radd rmul p + y -> x==y.
 Proof.
-elim p using Pos.peano_ind; simpl; intros.
+elim p using Pos.peano_ind; simpl; [intros H|intros ? H ?].
  apply S_inj; trivial.
  apply H.
    apply S_inj.
@@ -1710,8 +1717,8 @@ Lemma gen_phiN_inj x y :
   gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y ->
   x = y.
 Proof.
-destruct x; destruct y; simpl; intros; trivial.
- elim gen_phiPOS_not_0 with p.
+destruct x as [|p]; destruct y as [|p']; simpl; intros H; trivial.
+ elim gen_phiPOS_not_0 with p'.
    symmetry .
    rewrite (same_gen Rsth Reqe ARth); trivial.
  elim gen_phiPOS_not_0 with p.
@@ -1770,14 +1777,14 @@ Lemma gen_phiZ_inj x y :
   gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y ->
   x = y.
 Proof.
-destruct x; destruct y; simpl; intros.
+destruct x as [|p|p]; destruct y as [|p'|p']; simpl; intros H.
  trivial.
- elim gen_phiPOS_not_0 with p.
+ elim gen_phiPOS_not_0 with p'.
    rewrite (same_gen Rsth Reqe ARth).
    symmetry ; trivial.
- elim gen_phiPOS_not_0 with p.
+ elim gen_phiPOS_not_0 with p'.
    rewrite (same_gen Rsth Reqe ARth).
-   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')).
    rewrite <- H.
    apply (ARopp_zero Rsth Reqe ARth).
  elim gen_phiPOS_not_0 with p.
@@ -1790,12 +1797,12 @@ destruct x; destruct y; simpl; intros.
    rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
    rewrite H.
    apply (ARopp_zero Rsth Reqe ARth).
- elim gen_phiPOS_discr_sgn with p0 p.
+ elim gen_phiPOS_discr_sgn with p' p.
    symmetry ; trivial.
- replace p0 with p; trivial.
+ replace p' with p; trivial.
    apply gen_phiPOS_inject.
    rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)).
-   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p0)).
+   rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')).
    rewrite H; trivial.
    reflexivity.
 Qed.