]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/status.ml
the partial commit continues
[helm.git] / helm / software / helena / src / common / status.ml
index 3da988f8441eca5db3bc9f5aa687041ccc14087b..ec7f8a65c9bc1e3ee5dde0d9b49e8ee749b7008a 100644 (file)
@@ -14,7 +14,7 @@ module Q = Ccs
 
 type status = {
    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 *) 
@@ -23,7 +23,7 @@ type status = {
 (* helpers ******************************************************************)
 
 let initial_status () = {
-   delta = false; rt = false; 
+   delta = false; (* rt = false; *)
    si = !G.si; expand = !G.expand; cc = Q.init ()
 }