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/micromega/RMicromega.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/micromega')

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