On Thu, 16 Dec 2010, Michael Chan wrote:

Can you explain which messages are getting in the way in particular?

Mostly, the 'Unification bound exceeded' warnings. Exceeding the unification bound is an expected behaviour in my application, so I think it should be safe to suppress the warning at times. The main problem is that my system pretty prints out the tenv and tyenv when it pulls matchers from a sequence returned by Unify.matchers, but if I get a warning at a particular matcher, I lose the buffer containing the previous output.

Did yout try the tracing channel for your messages?


ProofGeneral mailing list

Reply via email to