| 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