Leonardo de Moura 9c8f57f322 fix: preserve info messages from candidates that failed to be elaborated ... @Kha Not sure whether we should have an option for supressing this information or not. We need this information for diagnosing problems. For example, I was trying to understand why the elaborator was looping. I suspected it was the TC module, but I was not getting any trace messages since the symbol was overloaded, and the case that did not work was the expensive one :(		2020-09-17 17:08:14 -07:00
..
Data	fix: preserve info messages from candidates that failed to be elaborated	2020-09-17 17:08:14 -07:00
Data.lean	chore: move RBTree and RBMap to Std	2020-06-25 13:26:16 -07:00
ShareCommon.lean	chore: move HashMap and HashSet to Std	2020-06-25 12:46:56 -07:00