| 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
                 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