moved the high level pretty printing setting to a toggle menu item of the View menu...

[helm.git] / matita / matita.ml

diff --git a/matita/matita.ml b/matita/matita.ml
index dc0aa579db5975ccbd4fab189c1f6de071b27929..ce9280dcdc229b6ceda080a4af4e55b12dca7858 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -214,10 +214,12 @@ let _ =
     );
     addDebugSeparator ();
 *)
+(* 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);
+*)
     addDebugItem "disable all (pretty printing) notations"
       (fun _ -> CicNotation.set_active_notations []);
     addDebugItem "enable all (pretty printing) notations"