From dadfbd96378d4c1b794ffc341bd10cc4d63b225d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 18 Dec 2011 23:56:06 +0000
Subject: Granted legitimate wish #2607 (not exposing crude fixpoint body of
 unfolded fixpoints when calling destruct). However, this might break
 compatibility.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Numbers/Natural/BigN/NMake_gen.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Numbers')

diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 3ea3d5fd5b..59d440c312 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -511,7 +511,7 @@ pr "
  solve_eval.
  destruct x as [ | xh xl ].
   simpl. unfold eval. rewrite make_op_S. rewrite nmake_op_S. auto.
- fold word in *.
+ simpl word in xh, xl |- *.
  unfold to_Z in *. rewrite make_op_WW.
  unfold eval in *. rewrite nmake_WW.
  f_equal; auto.
-- 
cgit v1.2.3