diff options
| author | Matthieu Sozeau | 2016-05-20 03:39:51 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 2c07b6d95c7b8fd754cdf9dd767dda989723125a (patch) | |
| tree | 089d115ad32ec20ca5dc0ac2f4d662fa279daed5 /kernel | |
| parent | 677d5deb72734a0e5502bcf47a905fcdf9374e51 (diff) | |
Typeclasses: verbosity and Limit Intros options
To deactivate the limitation of introductions (which was added to avoid
eta expansions in proof terms). This can cause huge blowups due to dumb
backtracking. The arrow introduction rule is reversible, so better do it
eagerly!
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions