- bug fix in the static disambiguation of unified binders

[helm.git] / helm / software / helena / src / basic_rg / brgGrafite.ml

diff --git a/helm/software/helena/src/basic_rg/brgGrafite.ml b/helm/software/helena/src/basic_rg/brgGrafite.ml
index bebd93bc759390d8c24fc88a4b4fc6c335996d01..c32747e00ce72c0e1fa2b12ebd9963d3c05a3440 100644 (file)
--- a/helm/software/helena/src/basic_rg/brgGrafite.ml
+++ b/helm/software/helena/src/basic_rg/brgGrafite.ml
@@ -9,6 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module F = Filename
 module P = Printf
 
 module U = NUri
@@ -22,6 +23,10 @@ module B = Brg
 
 let ok = ref true
 
+let base = "matita"
+
+let ext = ".ma"
+
 let width = 70
 
 let out_preamble och =
@@ -105,7 +110,9 @@ let rec out_term st p e och = function
 (* Interface functions ******************************************************)
 
 let open_out fname =
-   let och = open_out (fname ^ ".ma") in
+   let dir = F.concat !G.ma_dir base in 
+   let path = F.concat dir fname in
+   let och = open_out (path ^ ext) in
    out_preamble och;
    out_top_comment och (P.sprintf "This file is generated by %s: do not edit" G.version_string);
    out_include och "basics/pts";