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 *)
(* helpers ******************************************************************)
let initial_status () = {
- delta = false; rt = false;
+ delta = false; (* rt = false; *)
si = !G.si; expand = !G.expand; cc = Q.init ()
}