Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This mli is not part of the public interface and also never touched by the compiler, so it could be completely wrong without anyone noticing. Better to delete it than to pretend this is of any use.
- Loading branch information