diff options
| -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 f095a34821..866bc95b86 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -124,7 +124,7 @@ pr revert n. fix IHn 1. do 3 (destruct n; [unfold_ops; reflexivity|]). simpl mk_zn2z_ops_karatsuba. simpl word in *. - rewrite <- IHn. auto. + rewrite <- (IHn n). auto. Qed. (** * The main type [t], isomorphic with [exists n, word w0 n] *) |