Important commit:

[helm.git] / matita / matita.ml

diff --git a/matita/matita.ml b/matita/matita.ml
index 5717b710aa9925f48312e160b1c589884d22c13a..dc0aa579db5975ccbd4fab189c1f6de071b27929 100644 (file)
--- a/matita/matita.ml
+++ b/matita/matita.ml
@@ -214,6 +214,10 @@ let _ =
     );
     addDebugSeparator ();
 *)
+    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"