From 183112fc6a5fbb7d1c6d60b9717cdb8aceda78ca Mon Sep 17 00:00:00 2001
From: Pierre Boutillier
Date: Mon, 8 Sep 2014 16:19:39 +0200
Subject: Simpl less (so that cbn will not simpl too much)

---
 plugins/btauto/Reflect.v       | 6 +++---
 plugins/micromega/RMicromega.v | 5 ++---
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 8a95d5b4be..3bd7cd622c 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 d6f6748586..f4b4dd6612 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.
-- 
cgit v1.2.3