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)

---
 theories/Numbers/Natural/BigN/NMake.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Natural')

diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index bfbcb9465e..dab2399c9c 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.
-- 
cgit v1.2.3