- static disambiguation of Automath unified binders

[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 a076a9aae69e35dffee8b0cf570c9c8209346f12..bc04a5afdcdf58ef2f0bb0c53bb253ac1af24cff 100644 (file)
--- a/helm/software/helena/src/common/status.ml
+++ b/helm/software/helena/src/common/status.ml
@@ -9,22 +9,22 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
+module N = Level
 module G = Options
-module Q = Ccs
 
 type status = {
-   delta: bool;  (* global delta-expansion *)
-   si: bool;     (* sort inclusion *)
-(*   cc: Q.csys;   (* conversion constraints *) *)
+   delta: bool;    (* global delta-expansion *)
+   si: bool;       (* sort inclusion *)
+   lenv: N.status; (* level environment *)
 }
 
 (* helpers ******************************************************************)
 
 let initial_status () = {
    delta = false;
-   si = !G.si; (* cc = Q.init () *)
+   si = !G.si; lenv = N.initial_status ();
 }
 
 let refresh_status st = {st with
-   si = !G.si; (* cc = Q.init () *)
+   si = !G.si; lenv = N.initial_status ();
 }