diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 23:56:06 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-12-18 23:56:06 +0000 |
| commit | dadfbd96378d4c1b794ffc341bd10cc4d63b225d (patch) | |
| tree | 7ff1c2d295f7ff831302b92de6f00f686d0c9f3b /theories/Numbers/Natural | |
| parent | 5536b6d56226c4e53bbd6c5ae9a2c419c6f08874 (diff) | |
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
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 3ea3d5fd5..59d440c31 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. |