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/Cyclic/Abstract/NZCyclic.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers/Cyclic/Abstract')

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index c9f3a774dc..7594b0478a 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.
-- 
cgit v1.2.3