]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgHelena.ml
helena: updated prolog exportation to ld3 and ALT-0/PTS
[helm.git] / helm / software / helena / src / basic_rg / brgHelena.ml
index 07aa996013e7ff96655a5e0a32991cfb82574c92..43146aebb236db2af9379e88aec230c2fa3d5f72 100644 (file)
@@ -304,7 +304,6 @@ let close_out_tj3 och () =
       end
    in
    let chunks = out_list och 1 true size (List.rev !uris) in
-   out_clause och "main :- grundlagen.";
    KP.fprintf och "grundlagen :-\n";
    out_chunks och (pred chunks) 1;
    close_out och
@@ -325,10 +324,9 @@ let open_out_lp1 fname =
 let open_out_lp2 fname =
    let dir = KF.concat !G.manager_dir base in 
    let path = KF.concat dir fname in
-   let och = open_out (path ^ "2" ^ ext_lp) in
+   let och = open_out (path ^ "b_ld3" ^ ext_lp) in
    out_preamble och;
    out_top_comment och version;
-   out_clause och "accumulate helena.";
    output_entity_lp2 och, close_out_lp2 och
 
 let open_out_tj2 fname =