From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 9 Dec 2005 13:04:15 +0000 (+0000)
Subject: commented out some debugging prints
X-Git-Tag: make_still_working~8031
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c4b9695ec3ff5c35f7cfa8bf7df279558a3a8ca2;p=helm.git

commented out some debugging prints
---

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index e949020d9..0feab6121 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -340,7 +340,7 @@ object (self)
       | Some ((None, _, _, _, _, _) as info) ->
           (* building a dummy sequent for obj *)
           let t = self#find_obj_conclusion id in
-          HLog.debug (CicPp.ppterm t);
+(*           HLog.debug (CicPp.ppterm t); *)
           info, (~-1, [], t)
       | None -> assert false
     in
@@ -358,19 +358,19 @@ object (self)
                 let pattern =
                   ProofEngineHelpers.pattern_of ~term:ty [term]
                 in
-                HLog.debug (CicPp.ppname name ^ ":" ^ CicPp.ppterm pattern);
+(*                 HLog.debug (CicPp.ppname name ^ ":" ^ CicPp.ppterm pattern); *)
                 ~-1, [], pattern
             | Some (name, Cic.Def (bo, _)) ->
                 let pattern =
                   ProofEngineHelpers.pattern_of ~term:bo [term]
                 in
-                HLog.debug (CicPp.ppname name ^ ":=" ^ CicPp.ppterm pattern);
+(*                 HLog.debug (CicPp.ppname name ^ ":=" ^ CicPp.ppterm pattern); *)
                 ~-1, [], pattern)
             with Failure _ | Invalid_argument _ ->
               let pattern =
                 ProofEngineHelpers.pattern_of ~term:conclusion [term]
                 in
-                HLog.debug ("\\vdash " ^ CicPp.ppterm pattern);
+(*                 HLog.debug ("\\vdash " ^ CicPp.ppterm pattern); *)
                 ~-1, [], pattern)
       | _ -> assert false (* since it uses physical equality *)
     in