+ addDebugItem "disable high level pretty printer"
+ (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := true);
+ addDebugItem "enable high level pretty printer"
+ (fun _ -> CicMetaSubst.use_low_level_ppterm_in_context := false);
+(* ZACK moved to the View menu