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 0c15950edc..fb182720c9 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -365,7 +365,7 @@ pr " pp " Instance wn_spec (n:nat) : ZnZ.Specs (make_op n)."; pp " Proof."; - pp " intros n; elim n; clear n."; + pp " elim n; clear n."; pp " exact w%i_spec." (size + 1); pp " intros n Hrec; rewrite make_op_S."; pp " exact (mk_zn2z_specs_karatsuba Hrec)."; |