%auto_implicit has been renamed to %unbound_implicits

This commit is contained in:
Christian Rasmussen 2020-07-11 02:33:23 +02:00 committed by GitHub
parent b3bb73cfd6
commit 6211922960
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -280,7 +280,7 @@ names, e.g. in:
... where ``xs`` is a ``Vect n a``, it infers bindings for ``n`` and ``a``.
The ``%auto_implicits`` directive means that it will no longer automatically
The ``%unbound_implicits`` directive means that it will no longer automatically
bind names (that is, ``a`` and ``b`` in ``map`` above) but it will still
infer the types for any additional names, e.g. if you write: