X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FmrcOutput.ml;h=f39e07e03bb91c43b8a58aea713c02d3cc14a8c9;hp=19128fb6397a2eb0721d052a03672ba57871588a;hb=ae626612bff9c3746dd7647bbada791c737e348c;hpb=4d232392091ee233afc26ecf3120dd5f5c6a33c8

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
index 19128fb63..f39e07e03 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/mrcOutput.ml
@@ -48,10 +48,16 @@ let write_component st =
   write_mli cmod
 
 let write_index st =
+  let p = float (List.length st.ET.mods) in
+  let p =
+    if p > 0. then truncate (log10 p) else -1
+  in
+  let ps = Printf.sprintf "%%0%uu" (succ p) in
+  let fmt = Scanf.format_from_string ps "%u" in
   let cmod = Filename.concat st.ET.cdir "recommGc" in
   let och = open_out (cmod ^ ".ml") in
   let iter i name =
-    Printf.fprintf och "module G%03u = RecommGc%s\n" (succ i) name
+    Printf.fprintf och "module G%(%u%) = RecommGc%s\n" fmt (succ i) name
   in
   List.iteri iter st.ET.mods;
   close_out och;