]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgGallina.ml
= test2 for byte and opt
[helm.git] / helm / software / helena / src / basic_rg / brgGallina.ml
index d78f2a215b8bc4c9db4741e78f83e08ae9815ef9..bc65fe0752244f0c89c737f76c62f325baa57db1 100644 (file)
@@ -26,6 +26,8 @@ IFDEF MANAGER THEN
 
 let ok = ref true
 
+let version = KP.sprintf "This file was generated by %s: do not edit" (G.version_string true)
+
 let base = "coq"
 
 let ext = ".v"
@@ -130,7 +132,7 @@ let open_out fname =
    let path = KF.concat dir fname in
    let och = open_out (path ^ ext) 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;
    output_entity och, close_out och
 
 END