X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foptions.ml;h=b77757ddb6bbfb49e56ad17118aa44dac33238ae;hb=f72311aa07e71090a24eef9e4fb97cc2e95e6b16;hp=a2c749872e525f612b610152089373d35df123e2;hpb=aaafdf833247fc188049ab519d734d92f7e03333;p=helm.git

diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml
index a2c749872..b77757ddb 100644
--- a/helm/software/helena/src/common/options.ml
+++ b/helm/software/helena/src/common/options.ml
@@ -18,9 +18,15 @@ type kernel = Crg | Brg | Bag
 
 (* interface functions ******************************************************)
 
-let xdir = ref ""
+let stage = ref 3            (* stage *)
 
-let kernel = ref Brg
+let trace = ref 0            (* trace level *)
+
+let summary = ref false      (* log summary information *)
+
+let xdir = ref ""            (* directory for XML output *)
+
+let kernel = ref Brg         (* kernel type *)
 
 let si = ref false           (* use sort inclusion *)
 
@@ -57,6 +63,7 @@ let get_mk_uri () =
    fun s -> F.concat bu (s ^ ".ld")
 
 let clear () =
+   stage := 3; trace := 0; summary := false; 
    xdir := ""; kernel := Brg; si := false; cover := ""; 
    expand := false; indexes := false; icm := 0; unquote := false;
    debug_parser := false; debug_lexer := false