- bug fix in the static disambiguation of unified binders

[helm.git] / helm / software / helena / src / common / options.ml

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index 0c32d1138e775bb51c17ed21b47fc2b90e73741b..e7666efe3427cb323ec2fd9827d09f1de43100f6 100644 (file)
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 module F = Filename
+
 module C = Cps
 
 type uri_generator = string -> string
@@ -48,7 +49,9 @@ let debug_parser = ref false (* output parser debug information *)
 
 let debug_lexer = ref false  (* output lexer debug information *)
 
-let ma_preamble = ref ""     (* location of Matita preamble file *)
+let ma_dir = ref ""          (* directory for grafite output *)
+
+let ma_preamble = ref ""     (* location of grafite preamble file *)
 
 let kernel_id () = 
    let id = match !kernel with
@@ -71,4 +74,4 @@ let clear () =
    xdir := ""; kernel := Brg; si := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false;
    debug_parser := false; debug_lexer := false;
-   ma_preamble := ""
+   ma_dir := ""; ma_preamble := ""