Leonardo de Moura cab56d1e1b chore: do not invoke the hooks from addImported ... @Kha I am working on issue https://github.com/leanprover/lean4/issues/175 I am using solution 2 described there. The hooks will be at `AttrM` instead of `CoreM`. AFAICT code deleted by this commit is not necessary.		2020-09-21 16:28:07 -07:00
..
src	chore: do not invoke the hooks from addImported	2020-09-21 16:28:07 -07:00
stdlib	chore: do not invoke the hooks from addImported	2020-09-21 16:28:07 -07:00