]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/common/status.ml
- we removed a flag from the kernel status
[helm.git] / helm / software / helena / src / common / status.ml
index 89bf28e86e354dc3503c9c67cd16be77a41c87ba..401faf9aff450ec7936aba43b316661003a065d5 100644 (file)
@@ -13,7 +13,6 @@ module G = Options
 module N = Level
 
 type status = {
-   delta: bool;    (* global delta-expansion *)
    si: bool;       (* sort inclusion *)
    lenv: N.status; (* level environment *)
 }
@@ -21,10 +20,9 @@ type status = {
 (* helpers ******************************************************************)
 
 let initial_status () = {
-   delta = false;
    si = !G.si; lenv = N.initial_status ();
 }
 
 let refresh_status st = {st with
-   si = !G.si; lenv = N.initial_status ();
+   si = !G.si (*; lenv = N.initial_status (); *)
 }