]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgLP.ml
jet a change in dependences
[helm.git] / helm / software / helena / src / basic_rg / brgLP.ml
index ac7acd908eef7486713340914759e0661b2ba578..8a8f9d4f296d160550d91cf5e6320f26ce67f003 100644 (file)
@@ -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