Simpl less (so that cbn will not simpl too much)

19 files changed, 63 insertions, 67 deletions

diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 8a95d5b4b..3bd7cd622 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -196,9 +196,9 @@ Qed.
 Lemma make_last_nth_1 : forall A n i x def, i <> n ->
   list_nth i (@make_last A n x def) def = def.
 Proof.
-intros A n; induction n using Pos.peano_rect; intros i x def Hd; simpl.
-+ unfold make_last; rewrite Pos.peano_rect_base.
-  induction i using Pos.peano_case; [elim Hd; reflexivity|].
+intros A n; induction n using Pos.peano_rect; intros i x def Hd;
+  unfold make_last; simpl.
++ induction i using Pos.peano_case; [elim Hd; reflexivity|].
   rewrite list_nth_succ, list_nth_nil; reflexivity.
 + unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def).
   induction i using Pos.peano_case.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index d6f674858..f4b4dd661 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -243,7 +243,6 @@ Proof.
   unfold IQR ; intros.
   simpl.
   repeat rewrite mult_IZR.
-  simpl.  
   rewrite Pos2Nat.inj_mul.
   rewrite mult_INR.
   repeat INR_nat_of_P.
@@ -260,8 +259,8 @@ Proof.
   simpl.
   intros.
   unfold Qinv.
-  destruct x ; simpl in *.
-  destruct Qnum ; simpl.
+  destruct x.
+  destruct Qnum ; simpl in *.
   exfalso. auto with zarith.
   clear H.
   repeat INR_nat_of_P.
diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index 8cef48b69..a9d77c90d 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -110,7 +110,7 @@ Proof.
     split; split; auto with arith. inversion_clear 1. inversion H0.
   - (* n = (S (S n')) *)
     destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')).
-    split; split; simpl; rewrite ?double_S.
+    split; split; simpl div2; rewrite ?double_S.
     + inversion_clear 1. inversion_clear H0. auto.
     + injection 1. auto with arith.
     + inversion_clear 1. inversion_clear H0. auto.
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index fe08960ad..c9e5b8dd2 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1433,14 +1433,14 @@ Lemma flatten_e_elements :
  elements l ++ flatten_e (More x d r e) =
  elements (Node l x d r z) ++ flatten_e e.
 Proof.
- intros; simpl; apply elements_node.
+ intros; apply elements_node.
 Qed.
 
 Lemma cons_1 : forall (s:t elt) e,
   flatten_e (cons s e) = elements s ++ flatten_e e.
 Proof.
-  induction s; simpl; auto; intros.
-  rewrite IHs1; apply flatten_e_elements; auto.
+  induction s; auto; intros.
+  simpl flatten_e; rewrite IHs1; apply flatten_e_elements; auto.
 Qed.
 
 (** Proof of correction for the comparison *)
@@ -1478,7 +1478,7 @@ Lemma equal_cont_IfEq : forall m1 cont e2 l,
   (forall e, IfEq (cont e) l (flatten_e e)) ->
   IfEq (equal_cont cmp m1 cont e2) (elements m1 ++ l) (flatten_e e2).
 Proof.
- induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto.
+ induction m1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto.
  rewrite <- elements_node; simpl.
  apply Hl1; auto.
  clear e2; intros [|x2 d2 r2 e2].
@@ -2084,7 +2084,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
    (forall e, Cmp (cont e) l (P.flatten_e e)) ->
    Cmp (compare_cont s1 cont e2) (R.elements s1 ++ l) (P.flatten_e e2).
   Proof.
-   induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; simpl; intros; auto.
+   induction s1 as [|l1 Hl1 x1 d1 r1 Hr1 h1]; intros; auto.
    rewrite <- P.elements_node; simpl.
    apply Hl1; auto. clear e2. intros [|x2 d2 r2 e2].
    simpl; auto.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index d1d9897fb..154c2384c 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -1019,7 +1019,7 @@ Lemma flatten_e_elements :
  forall l x r c e,
  elements l ++ flatten_e (More x r e) = elements (Node c l x r) ++ flatten_e e.
 Proof.
- intros; simpl. now rewrite elements_node, app_ass.
+ intros. now rewrite elements_node, app_ass.
 Qed.
 
 Lemma cons_1 : forall s e,
@@ -1053,7 +1053,7 @@ Lemma compare_cont_Cmp : forall s1 cont e2 l,
  (forall e, Cmp (cont e) l (flatten_e e)) ->
  Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
 Proof.
- induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; simpl; intros; auto.
+ induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; intros; auto.
  rewrite elements_node, app_ass; simpl.
  apply Hl1; auto. clear e2. intros [|x2 r2 e2].
  simpl; auto.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index d7e56cdef..751d4f35c 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -987,7 +987,7 @@ Proof.
     rewrite app_length, <- elements_cardinal. simpl.
     rewrite Nat.add_succ_r, <- Nat.succ_le_mono.
     apply Nat.add_le_mono_l. }
- simpl. rewrite elements_node, app_ass. now subst.
+ rewrite elements_node, app_ass. now subst.
 Qed.
 
 Lemma treeify_aux_spec n (p:bool) :
@@ -1012,7 +1012,7 @@ Qed.
 Lemma plength_aux_spec l p :
   Pos.to_nat (plength_aux l p) = length l + Pos.to_nat p.
 Proof.
- revert p. induction l; simpl; trivial.
+ revert p. induction l; trivial. simpl plength_aux.
  intros. now rewrite IHl, Pos2Nat.inj_succ, Nat.add_succ_r.
 Qed.
 
@@ -1058,7 +1058,7 @@ Lemma filter_aux_elements s f acc :
  filter_aux f s acc = List.filter f (elements s) ++ acc.
 Proof.
  revert acc.
- induction s as [|c l IHl x r IHr]; simpl; trivial.
+ induction s as [|c l IHl x r IHr]; trivial.
  intros acc.
  rewrite elements_node, filter_app. simpl.
  destruct (f x); now rewrite IHl, IHr, app_ass.
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 94242394b..6551f6c10 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -84,8 +84,8 @@ Qed.
 Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a).
 Proof.
  destruct a as [|[p|p| ]]; trivial.
- - simpl N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double.
- - simpl N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double.
+ - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double.
+ - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double.
 Qed.
 
 Lemma inj_compare a a' :
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index c9f3a774d..7594b0478 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -106,7 +106,7 @@ Qed.
 
 Theorem one_succ : one == succ zero.
 Proof.
-zify; simpl. now rewrite one_mod_wB.
+zify; simpl Z.add. now rewrite one_mod_wB.
 Qed.
 
 Theorem two_succ : two == succ one.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
index 35d8b595c..e14c3b829 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
@@ -194,9 +194,9 @@ Section DoubleAdd.
 
   Lemma spec_ww_add_c  : forall x y, [+[ww_add_c x y]] = [[x]] + [[y]].
   Proof.
-   destruct x as [ |xh xl];simpl;trivial.
-   destruct y as [ |yh yl];simpl. rewrite Z.add_0_r;trivial.
-   replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]))
+   destruct x as [ |xh xl];trivial.
+   destruct y as [ |yh yl]. rewrite Z.add_0_r;trivial.
+   simpl. replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]))
    with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|])). 2:ring.
    generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l];
     intros H;unfold interp_carry in H;rewrite <- H.
@@ -218,10 +218,11 @@ Section DoubleAdd.
 
    Lemma spec_ww_add_c_cont  : P x y (ww_add_c_cont x y).
    Proof.
-    destruct x as [ |xh xl];simpl;trivial.
+    destruct x as [ |xh xl];trivial.
     apply spec_f0;trivial.
-    destruct y as [ |yh yl];simpl.
-    apply spec_f0;simpl;rewrite Z.add_0_r;trivial.
+    destruct y as [ |yh yl].
+    apply spec_f0;rewrite Z.add_0_r;trivial.
+    simpl.
     generalize (spec_w_add_c xl yl);destruct (w_add_c xl yl) as [l|l];
      intros H;unfold interp_carry in H.
     generalize (spec_w_add_c xh yh);destruct (w_add_c xh yh) as [h|h];
@@ -234,10 +235,10 @@ Section DoubleAdd.
      as [h|h]; intros H1;unfold interp_carry in *.
     apply spec_f0;simpl;rewrite H1. rewrite Z.mul_add_distr_r.
     rewrite <- Z.add_assoc;rewrite H;ring.
-    apply spec_f1.  simpl;rewrite spec_w_WW;rewrite wwB_wBwB.
+    apply spec_f1. rewrite spec_w_WW;rewrite wwB_wBwB.
     rewrite Z.add_assoc; rewrite Z.pow_2_r; rewrite <- Z.mul_add_distr_r.
     rewrite Z.mul_1_l in H1;rewrite H1. rewrite Z.mul_add_distr_r.
-    rewrite <- Z.add_assoc;rewrite H;ring.
+    rewrite <- Z.add_assoc;rewrite H; simpl; ring.
    Qed.
 
   End Cont.
@@ -245,11 +246,11 @@ Section DoubleAdd.
   Lemma spec_ww_add_carry_c :
          forall x y, [+[ww_add_carry_c x y]] = [[x]] + [[y]] + 1.
   Proof.
-   destruct x as [ |xh xl];intro y;simpl.
+   destruct x as [ |xh xl];intro y.
    exact (spec_ww_succ_c y).
-   destruct y as [ |yh yl];simpl.
+   destruct y as [ |yh yl].
    rewrite Z.add_0_r;exact (spec_ww_succ_c (WW xh xl)).
-   replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1)
+   simpl; replace ([|xh|] * wB + [|xl|] + ([|yh|] * wB + [|yl|]) + 1)
    with (([|xh|]+[|yh|])*wB + ([|xl|]+[|yl|]+1)). 2:ring.
    generalize (spec_w_add_carry_c xl yl);destruct (w_add_carry_c xl yl)
     as [l|l];intros H;unfold interp_carry in H;rewrite <- H.
@@ -281,7 +282,7 @@ Section DoubleAdd.
 
   Lemma spec_ww_add : forall x y, [[ww_add x y]] = ([[x]] + [[y]]) mod wwB.
   Proof.
-   destruct x as [ |xh xl];intros y;simpl.
+   destruct x as [ |xh xl];intros y.
    rewrite Zmod_small;trivial. apply spec_ww_to_Z;trivial.
    destruct y as [ |yh yl].
    change [[W0]] with 0;rewrite Z.add_0_r.
@@ -299,7 +300,7 @@ Section DoubleAdd.
   Lemma spec_ww_add_carry :
 	 forall x y, [[ww_add_carry x y]] = ([[x]] + [[y]] + 1) mod wwB.
   Proof.
-   destruct x as [ |xh xl];intros y;simpl.
+   destruct x as [ |xh xl];intros y.
    exact (spec_ww_succ y).
    destruct y as [ |yh yl].
    change [[W0]] with 0;rewrite Z.add_0_r. exact (spec_ww_succ (WW xh xl)).
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
index dddae7db5..20b55a4c6 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
@@ -97,8 +97,7 @@ Section POS_MOD.
  assert (HHHHH:= lt_0_wB w_digits).
  assert (F0: forall x y, x - y + y = x); auto with zarith.
  intros w1 p; case (spec_to_w_Z p); intros HH1 HH2.
- unfold ww_pos_mod; case w1.
- simpl; rewrite Zmod_small; split; auto with zarith.
+ unfold ww_pos_mod; case w1. reflexivity.
  intros xh xl; rewrite spec_ww_compare.
     case Z.compare_spec;
     rewrite spec_w_0W; rewrite spec_zdigits; fold wB;
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
index 789436334..5ca332551 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
@@ -266,8 +266,8 @@ Section DoubleSqrt.
       if ww_is_even x then [[x]] mod 2 = 0 else [[x]] mod 2 = 1.
 clear spec_more_than_1_digit.
 intros x; case x; simpl ww_is_even.
+ reflexivity.
  simpl.
- rewrite Zmod_small; auto with zarith.
  intros w1 w2; simpl.
  unfold base.
  rewrite Zplus_mod; auto with zarith.
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
index 900cb1db5..fad488beb 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
@@ -14,6 +14,7 @@ Require Import ZArith.
 Local Open Scope Z_scope.
 
 Definition base digits := Z.pow 2 (Zpos digits).
+Arguments base digits: simpl never.
 
 Section Carry.
 
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 98f84a60c..f6669d284 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -1414,7 +1414,7 @@ Section Int31_Specs.
  generalize (phi_bounded a1)(phi_bounded a2)(phi_bounded b); intros.
  assert ([|b|]>0) by (auto with zarith).
  generalize (Z_div_mod (phi2 a1 a2) [|b|] H4) (Z_div_pos (phi2 a1 a2) [|b|] H4).
- unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]); simpl.
+ unfold Z.div; destruct (Z.div_eucl (phi2 a1 a2) [|b|]).
  rewrite ?phi_phi_inv.
  destruct 1; intros.
  unfold phi2 in *.
@@ -1444,7 +1444,7 @@ Section Int31_Specs.
  unfold div31; intros.
  assert ([|b|]>0) by (auto with zarith).
  generalize (Z_div_mod [|a|] [|b|] H0) (Z_div_pos [|a|] [|b|] H0).
- unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]); simpl.
+ unfold Z.div; destruct (Z.div_eucl [|a|] [|b|]).
  rewrite ?phi_phi_inv.
  destruct 1; intros.
  rewrite H1, Z.mul_comm.
@@ -1467,7 +1467,7 @@ Section Int31_Specs.
  assert ([|b|]>0) by (auto with zarith).
  unfold Z.modulo.
  generalize (Z_div_mod [|a|] [|b|] H0).
- destruct (Z.div_eucl [|a|] [|b|]); simpl.
+ destruct (Z.div_eucl [|a|] [|b|]).
  rewrite ?phi_phi_inv.
  destruct 1; intros.
  generalize (phi_bounded b); intros.
@@ -1480,15 +1480,14 @@ Section Int31_Specs.
   unfold gcd31.
   induction (2*size)%nat; intros.
   reflexivity.
-  simpl.
+  simpl euler.
   unfold compare31.
   change [|On|] with 0.
   generalize (phi_bounded j)(phi_bounded i); intros.
   case_eq [|j|]; intros.
   simpl; intros.
   generalize (Zabs_spec [|i|]); omega.
-  simpl.
-  rewrite IHn, H1; f_equal.
+  simpl. rewrite IHn, H1; f_equal.
   rewrite spec_mod, H1; auto.
   rewrite H1; compute; auto.
   rewrite H1 in H; destruct H as [H _]; compute in H; elim H; auto.
@@ -1521,7 +1520,7 @@ Section Int31_Specs.
  simpl; auto.
  simpl; intros.
  case_eq (firstr i); intros H; rewrite 2 IHn;
-  unfold phibis_aux; simpl; rewrite H; fold (phibis_aux n (shiftr i));
+  unfold phibis_aux; simpl; rewrite ?H; fold (phibis_aux n (shiftr i));
   generalize (phibis_aux_pos n (shiftr i)); intros;
   set (z := phibis_aux n (shiftr i)) in *; clearbody z;
   rewrite <- nat_rect_plus.
@@ -1575,10 +1574,9 @@ Section Int31_Specs.
  clear p H; revert x y.
 
  induction n.
- simpl; intros.
- change (Z.pow_pos 2 31) with (2^31).
+ simpl Z.of_nat; intros.
  rewrite Z.mul_1_r.
- replace ([|y|] / 2^31) with 0.
+ replace ([|y|] / 2^(31-0)) with 0.
  rewrite Z.add_0_r.
  symmetry; apply Zmod_small; apply phi_bounded.
  symmetry; apply Zdiv_small; apply phi_bounded.
@@ -1666,7 +1664,7 @@ Section Int31_Specs.
  Proof.
   intros.
   generalize (phi_inv_phi x).
-  rewrite H; simpl.
+  rewrite H; simpl phi_inv.
   intros H'; rewrite <- H'.
   simpl; auto.
  Qed.
@@ -1774,7 +1772,7 @@ Section Int31_Specs.
  Proof.
   intros.
   generalize (phi_inv_phi x).
-  rewrite H; simpl.
+  rewrite H; simpl phi_inv.
   intros H'; rewrite <- H'.
   simpl; auto.
  Qed.
@@ -2121,7 +2119,7 @@ Section Int31_Specs.
  unfold phi2; rewrite Hc1.
  assert (0 <= [|il|]/[|j|]) by (apply Z_div_pos; auto with zarith).
  rewrite Z.mul_comm, Z_div_plus_full_l; unfold base; auto with zarith.
- unfold Z.pow, Z.pow_pos in Hj1; simpl in Hj1; auto with zarith.
+ simpl wB in Hj1. unfold Z.pow_pos in Hj1. simpl in Hj1. auto with zarith.
  case (Z.le_gt_cases (2 ^ 30) [|j|]); intros Hjj.
  rewrite spec_compare; case Z.compare_spec;
   rewrite div312_phi; auto; intros Hc;
@@ -2260,9 +2258,8 @@ Section Int31_Specs.
  intros Hihl1.
  generalize (spec_sub_c il il1).
  case sub31c; intros il2 Hil2.
- simpl interp_carry in Hil2.
  rewrite spec_compare; case Z.compare_spec.
- unfold interp_carry.
+ unfold interp_carry in *.
  intros H1; split.
  rewrite Z.pow_2_r, <- Hihl1.
  unfold phi2; ring[Hil2 H1].
@@ -2279,7 +2276,7 @@ Section Int31_Specs.
  rewrite Z.mul_add_distr_r, Z.add_0_r; auto with zarith.
  case (phi_bounded il1); intros H3 _.
  apply Z.add_le_mono; auto with zarith.
- unfold interp_carry; change (1 * 2 ^ Z.of_nat size) with base.
+ unfold interp_carry in *; change (1 * 2 ^ Z.of_nat size) with base.
  rewrite Z.pow_2_r, <- Hihl1, Hil2.
  intros H1.
  rewrite <- Z.le_succ_l, <- Z.add_1_r in H1.
@@ -2383,8 +2380,8 @@ Qed.
 
  Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x|] = 0.
  Proof.
- clear; unfold ZnZ.eq0; simpl.
- unfold compare31; simpl; intros.
+ clear; unfold ZnZ.eq0, int31_ops.
+ unfold compare31; intros.
  change [|0|] with 0 in H.
  apply Z.compare_eq.
  now destruct ([|x|] ?= 0).
@@ -2395,7 +2392,7 @@ Qed.
  Lemma spec_is_even : forall x,
       if ZnZ.is_even x then [|x|] mod 2 = 0 else [|x|] mod 2 = 1.
  Proof.
- unfold ZnZ.is_even; simpl; intros.
+ unfold ZnZ.is_even, int31_ops; intros.
  generalize (spec_div x 2).
  destruct (x/2)%int31 as (q,r); intros.
  unfold compare31.
@@ -2420,7 +2417,7 @@ Qed.
 
  Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x|] [|y|].
  Proof.
- unfold ZnZ.lor; simpl. unfold lor31.
+ unfold ZnZ.lor,int31_ops. unfold lor31.
  rewrite phi_phi_inv.
  apply Z.mod_small; split; trivial.
  - apply Z.lor_nonneg; split; apply phi_bounded.
@@ -2431,7 +2428,7 @@ Qed.
 
  Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x|] [|y|].
  Proof.
- unfold ZnZ.land; simpl. unfold land31.
+ unfold ZnZ.land, int31_ops. unfold land31.
  rewrite phi_phi_inv.
  apply Z.mod_small; split; trivial.
  - apply Z.land_nonneg; left; apply phi_bounded.
@@ -2443,7 +2440,7 @@ Qed.
 
  Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x|] [|y|].
  Proof.
- unfold ZnZ.lxor; simpl. unfold lxor31.
+ unfold ZnZ.lxor, int31_ops. unfold lxor31.
  rewrite phi_phi_inv.
  apply Z.mod_small; split; trivial.
  - apply Z.lxor_nonneg; split; intros; apply phi_bounded.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index bfbcb9465..dab2399c9 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -146,7 +146,7 @@ Module Make (W0:CyclicType) <: NType.
  Theorem spec_add: forall x y, [add x y] = [x] + [y].
  Proof.
   intros x y. rewrite add_fold. apply spec_same_level; clear x y.
-  intros n x y. simpl.
+  intros n x y. cbv beta iota zeta.
   generalize (ZnZ.spec_add_c x y); case ZnZ.add_c; intros z H.
   rewrite spec_mk_t. assumption.
   rewrite spec_mk_t_S. unfold interp_carry in H.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index a30c555c1..0f794c513 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -649,7 +649,7 @@ Theorem sub_mask_carry_spec p q :
   sub_mask_carry p q = pred_mask (sub_mask p q).
 Proof.
   revert q. induction p as [p IHp|p IHp| ]; destruct q; simpl;
-   try reflexivity; try rewrite IHp;
+   try reflexivity; rewrite ?IHp;
    destruct (sub_mask p q) as [|[r|r| ]|] || destruct p; auto.
 Qed.
 
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v
index fcc12ab45..44b9e7d03 100644
--- a/theories/PArith/BinPosDef.v
+++ b/theories/PArith/BinPosDef.v
@@ -537,7 +537,7 @@ Definition iter_op {A}(op:A->A->A) :=
   end.
 
 Definition to_nat (x:positive) : nat := iter_op plus x (S O).
-
+Arguments to_nat x: simpl never.
 (** ** From Peano natural numbers to binary positive numbers *)
 
 (** A version preserving positive numbers, and sending 0 to 1. *)
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v
index 4336d47af..0f2ecf55a 100644
--- a/theories/PArith/Pnat.v
+++ b/theories/PArith/Pnat.v
@@ -196,7 +196,8 @@ Theorem inj_iter :
 Proof.
  induction p using peano_ind.
  - trivial.
- - intros. rewrite inj_succ, iter_succ. simpl. now f_equal.
+ - intros. rewrite inj_succ, iter_succ. 
+  simpl. f_equal. apply IHp.
 Qed.
 
 End Pos2Nat.
@@ -210,7 +211,7 @@ Module Nat2Pos.
 Theorem id (n:nat) : n<>0 -> Pos.to_nat (Pos.of_nat n) = n.
 Proof.
  induction n as [|n H]; trivial. now destruct 1.
- intros _. simpl. destruct n. trivial.
+ intros _. simpl Pos.of_nat. destruct n. trivial.
  rewrite Pos2Nat.inj_succ. f_equal. now apply H.
 Qed.
 
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 319e2c269..23b692022 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -59,7 +59,7 @@ Section Log_pos. (* Log of positive integers *)
 
   Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p.
   Proof.
-   induction p; simpl.
+   induction p; simpl log_sup.
    - change (Zpos p~1) with (2*(Zpos p)+1).
      rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy.
      unfold Z.succ. now rewrite !(Z.add_comm _ 1), Z.add_assoc.
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 8ff641a33..5b0e3ef5e 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -152,10 +152,8 @@ Qed.
 Theorem Zpow_mod_correct a m n :
  n <> 0 -> Zpow_mod a m n = (a ^ m) mod n.
 Proof.
-  intros Hn. destruct m; simpl.
-  - trivial.
+  intros Hn. destruct m; simpl; trivial.
   - apply Zpow_mod_pos_correct; auto with zarith.
-  - rewrite Z.mod_0_l; auto with zarith.
 Qed.
 
 (* Complements about power and number theory. *)