@@ -163,7 +163,7 @@ If the goal type turns out to have been the unit type, we fill using the unit co
163163Otherwise, we fail with an error message informing the user that the current goal is not trivial.
164164
165165Additionally, 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.
167167The 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.
168168
169169Changing the Global Context