aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Natural/BigN/NMake_gen.ml
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Natural/BigN/NMake_gen.ml')
-rw-r--r--theories/Numbers/Natural/BigN/NMake_gen.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index c360f53dc8..7424d877bb 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -139,7 +139,6 @@ let _ =
pr "";
pr " Definition %s := %s_." t t;
pr "";
- pr " Typeclasses unfold %s." t;
pr " Definition w_0 := w0_op.(znz_0).";
pr "";