diff options
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. |