Pretty-printing width is now configurable, default is 80.

generator/main.ml

@@ -24,6 +24,21 @@ let outputfile = ref None
 
 (*#########################################################################*)
 
+let spec =
+  Arg.align [
+    ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs), 
+                      " includes a directory where to look for interface files");
+    ("-pure", Arg.Set Characteristic.pure_mode, " generate formulae for purely-functional code");
+    ("-rectypes", Arg.Set Clflags.recursive_types, " activates recursive types");
+    ("-credits", Arg.Set Characteristic.use_credits, " generate 'pay' instructions");
+    ("-nostdlib", Arg.Set no_mystd_include, " do not include standard library");
+    ("-nopervasives", Arg.Set Clflags.nopervasives, " do not include standard pervasives file");
+    ("-o", Arg.String (fun s -> outputfile := Some s), " set the output file name");
+    ("-onlycmj", Arg.Set onlycmj, " only generate the .cmj file, not the .v file");
+    ("-debug", Arg.Set is_tracing, " trace the various steps");
+    ("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file");
+  ]
+
 let _ =
    Settings.configure();
 
@@ -31,16 +46,7 @@ let _ =
    trace "1) parsing of command line";
    let files = ref [] in
    Arg.parse  
-     [ ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs), 
-                      "includes a directory where to look for interface files");
-       ("-pure", Arg.Set Characteristic.pure_mode, "generate formulae for purely-functional code");
-       ("-rectypes", Arg.Set Clflags.recursive_types, "activates recursive types");
-       ("-credits", Arg.Set Characteristic.use_credits, "generate 'pay' instructions");
-       ("-nostdlib", Arg.Set no_mystd_include, "do not include standard library");
-       ("-nopervasives", Arg.Set Clflags.nopervasives, "do not include standard pervasives file");
-       ("-o", Arg.String (fun s -> outputfile := Some s), "set the output file name");
-       ("-onlycmj", Arg.Set onlycmj, "only generate the cmj file, not the coq file");
-       ("-debug", Arg.Set is_tracing, "trace the various steps") ]
+     spec
      (fun f -> files := f::!files)
      ("usage: [-I dir] [..other options..] file.ml");
    (*

generator/print_coq.ml

@@ -19,7 +19,7 @@ let indentation =
   2
 
 let width =
-  80
+  ref 80
 
 (* -------------------------------------------------------------------------- *)
 
@@ -442,5 +442,5 @@ let tops ts =
 (* The main entry point translates a list of toplevel elements to a string. *)
 
 let tops ts : string =
-  run (PPrintEngine.ToBuffer.pretty 0.9 width) (tops ts)
+  run (PPrintEngine.ToBuffer.pretty 0.9 !width) (tops ts)