Ctype: allow equation generation while computing type equality
Fix equality equations
Env: strengthen implicit modules on registration
Implicitsearch: equation based resolution procedure
Ctype: fix typo
Typemod: check that implicit modules are closed