]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/status.ml
new message reporting system improves performance significatively
[helm.git] / helm / software / helena / src / common / status.ml
index e9c6e5620f9866564b3236a144c8ca260362a8c1..3ae3136089d6ae9239bf571217c14df9dd80c01f 100644 (file)
@@ -13,22 +13,18 @@ module G = Options
 module Q = Ccs
 
 type status = {
-   ll: int;      (* log level *)
    delta: bool;  (* global delta-expansion *)
-   rt: bool;     (* reference typing *)
    si: bool;     (* sort inclusion *)
-   expand: bool; (* always expand global definitions *)
    cc: Q.csys;   (* conversion constraints *)
-   tc: bool;     (* trace constraints *)
 }
 
 (* helpers ******************************************************************)
 
 let initial_status () = {
-   ll = 0; delta = false; rt = false; tc = false;
-   si = !G.si; expand = !G.expand; cc = Q.init ()
+   delta = false;
+   si = !G.si; cc = Q.init ()
 }
 
 let refresh_status st = {st with
-   si = !G.si; expand = !G.expand; cc = Q.init ()
+   si = !G.si; cc = Q.init ()
 }