X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgLP.ml;h=8a8f9d4f296d160550d91cf5e6320f26ce67f003;hb=fdb80b08af83b86759833142456ce3c4f84cd80e;hp=ac7acd908eef7486713340914759e0661b2ba578;hpb=e7cbf3ee4fc73e3e95f337f020186652315cf4a8;p=helm.git

diff --git a/helm/software/helena/src/basic_rg/brgLP.ml b/helm/software/helena/src/basic_rg/brgLP.ml
index ac7acd908..8a8f9d4f2 100644
--- a/helm/software/helena/src/basic_rg/brgLP.ml
+++ b/helm/software/helena/src/basic_rg/brgLP.ml
@@ -24,6 +24,8 @@ IFDEF MANAGER THEN
 
 (* Internal functions *******************************************************)
 
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
 let ok = ref true
 
 let uris = ref []
@@ -192,14 +194,14 @@ let output_entity_tj2 och st (_, na, u, b) =
       let dir, name = mk_name !chunk in
       let soch = open_out (KF.concat dir name ^ ext_tj_sig) in
       out_preamble soch;
-      out_top_comment soch (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+      out_top_comment soch version;
       out_clause soch (KP.sprintf "sig %s." name);
       out_clause soch "accum_sig grundlagen.";
       out_clause soch (KP.sprintf "type line+%02u t -> int -> t -> o." !chunk);
       close_out soch;
       let soch = open_out (KF.concat dir name ^ ext_tj) in
       out_preamble soch;
-      out_top_comment soch (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+      out_top_comment soch version;
       out_clause soch (KP.sprintf "module %s." name);
       sub_och := soch
    end;
@@ -314,7 +316,8 @@ let open_out_lp1 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "1" ^ ext_lp) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
+   out_clause och "accumulate helena.";
    out_clause och "main :- grundlagen.";
    out_clause och "grundlagen :- gv+";
    output_entity_lp1 och, close_out_lp1 och
@@ -324,7 +327,8 @@ let open_out_lp2 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "2" ^ ext_lp) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
+   out_clause och "accumulate helena.";
    output_entity_lp2 och, close_out_lp2 och
 
 let open_out_tj2 fname =
@@ -332,7 +336,7 @@ let open_out_tj2 fname =
    let path = KF.concat dir fname ^ "2" in
    let och = open_out (path ^ ext_tj) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
    out_clause och "module grundlagen.";
    output_entity_tj2 och, close_out_tj2 och
 
@@ -341,7 +345,7 @@ let open_out_tj3 fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ "3" ^ ext_tj) in
    out_preamble och;
-   out_top_comment och (KP.sprintf "This file was generated by %s: do not edit" G.version_string);
+   out_top_comment och version;
    out_clause och "module grundlagen.";
    out_clause och "accumulate helena.";
    output_entity_tj3 och, close_out_tj3 och