]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.ml
commented out some debugging prints
[helm.git] / helm / matita / matitaMathView.ml
index e949020d93c65b7a3d7f4820859e4fe63fa91981..0feab6121278a5787e965564b9042275de19d7bd 100644 (file)
@@ -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