diff --git a/docs/source/app/interfaces.rst b/docs/source/app/interfaces.rst
index 11d6b9a9e..553937a2e 100644
--- a/docs/source/app/interfaces.rst
+++ b/docs/source/app/interfaces.rst
@@ -50,7 +50,7 @@ use ``PrimIO`` in the initial list of errors ``Init``.
 
 .. code-block:: idris
 
-    HasErr Void e => PrimIO e where ...
+    HasErr AppHasIO e => PrimIO e where ...
 
 Given this, we can implement ``Console`` and run our ``hello``
 program in ``IO``. It is implemented as follows in ``Control.App.Console``:
diff --git a/docs/source/app/introapp.rst b/docs/source/app/introapp.rst
index de756efa3..9997eca18 100644
--- a/docs/source/app/introapp.rst
+++ b/docs/source/app/introapp.rst
@@ -95,7 +95,7 @@ synonym for ``Type``):
 .. code-block:: idris
 
     Init : List Error
-    Init = [Void]
+    Init = [AppHasIO]
 
     run : App {l} Init a -> IO a
 
@@ -103,5 +103,5 @@ Generalising the ``Path`` parameter with ``l``
 means that we can invoke ``run`` for any application, whether the ``Path``
 is ``NoThrow`` or ``MayThrow``. But, in practice, all applications
 given to ``run`` will not throw at the top level, because the only
-exception type available is the empty type ``Void``. Any exceptions
+exception type available is the type ``AppHasIO``. Any exceptions
 will have been introduced and handled inside the ``App``.