- commit completed :)

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

diff --git a/helm/software/helena/src/common/status.ml b/helm/software/helena/src/common/status.ml
index ec7f8a65c9bc1e3ee5dde0d9b49e8ee749b7008a..e9c6e5620f9866564b3236a144c8ca260362a8c1 100644 (file)
--- a/helm/software/helena/src/common/status.ml
+++ b/helm/software/helena/src/common/status.ml
@@ -13,21 +13,22 @@ module G = Options
 module Q = Ccs
 
 type status = {
+   ll: int;      (* log level *)
    delta: bool;  (* global delta-expansion *)
-(*   rt: bool;     (* reference typing *) *)
+   rt: bool;     (* reference typing *)
    si: bool;     (* sort inclusion *)
    expand: bool; (* always expand global definitions *)
-   cc: Q.csys;   (* conversion constraints *) 
+   cc: Q.csys;   (* conversion constraints *)
+   tc: bool;     (* trace constraints *)
 }
 
 (* helpers ******************************************************************)
 
 let initial_status () = {
-   delta = false; (* rt = false; *)
+   ll = 0; delta = false; rt = false; tc = false;
    si = !G.si; expand = !G.expand; cc = Q.init ()
 }
 
 let refresh_status st = {st with
    si = !G.si; expand = !G.expand; cc = Q.init ()
 }
-