+*)
+(* ZACK: moved to a check box menu item in the View menu
+ 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);