idris-lang/Idris-dev — pull request #1450 by david-christiansen (2014-07-31 12:07:55+00:00)
Title: Don't show irrelevant MNs in prover

Previously, proof steps like applyTactic would introduce MNs to the
proof state, with names like {scriptVar231}. This change hides those, as
the user cannot type them anyway.

If they are used in a later assumption, then they will be shown anyway.