| Thu, 24 Jul 2014 20:21:59 +0200 | kuncar | having extra assumptions (typically from a context) means there is no chance to have a valid code equation => skip decoding and registration of the code equations | changeset | files |
| Thu, 24 Jul 2014 20:21:34 +0200 | kuncar | store explicitly quotient types with no_code => more precise registration of code equations | changeset | files |