[ doc, tiny ] Correct wrong directive for unbound implicits turning off

buzden · Sep 29, 2023 · d6ce35f · d6ce35f
1 parent 63ee39b
commit d6ce35f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/docs/source/faq/faq.rst b/docs/source/faq/faq.rst
@@ -269,7 +269,7 @@ directive:
 
 .. code-block:: idris
 
-    %auto_implicits off
+    %unbound_implicits off
 
 In this case, you can bind ``n`` and ``m`` as implicits, but not ``ty``,
 as follows: