Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
docs: remove docstring from implicitDefEqProofs
this option was added in fb97275 to prepare for #4595, due to boostrapping issues, but #4595 has not landed yet. This is be very confusing when people discover this option and try to use it (as I did). So let's clearly mark this as not yet implemented on `main`.
- Loading branch information