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

3 files changed, 5 insertions, 4 deletions

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.