@@ -163,7 +163,7 @@ If the goal type turns out to have been the unit type, we fill using the unit co
163Otherwise, we fail with an error message informing the user that the current goal is not trivial.
163Otherwise, we fail with an error message informing the user that the current goal is not trivial.
165Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
165Additionally, the elaboration state can be dumped into an error message with the ``debug`` tactic.
166−A variant, ``debugMessage``, allows arbitrary messages to be included with the state, allowing for a kind of "``printf`` debuggging" of elaboration scripts.
166+A variant, ``debugMessage``, allows arbitrary messages to be included with the state, allowing for a kind of "``printf`` debugging" of elaboration scripts.
167The message format used by ``debugMessage`` is the same for errors produced by the error reflection mechanism, allowing the re-use of the Idris pretty-printer when rendering messages.
167The message format used by ``debugMessage`` is the same for errors produced by the error reflection mechanism, allowing the re-use of the Idris pretty-printer when rendering messages.
169Changing the Global Context
169Changing the Global Context