module N = Level
type status = {
- delta: bool; (* global delta-expansion *)
si: bool; (* sort inclusion *)
lenv: N.status; (* level environment *)
}
(* 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 (); *)
}