summaryrefslogtreecommitdiff
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.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 4d6b45c5..04c7b96d 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -8,7 +8,7 @@
(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
(************************************************************************)
-(*i $Id: NMake_gen.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
+(*i $Id: NMake_gen.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
(*S NMake_gen.ml : this file generates NMake.v *)
@@ -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 "";