diff options
| author | Hugo Herbelin | 2017-04-26 12:15:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-28 16:39:54 +0200 |
| commit | 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /pretyping/typeclasses_errors.mli | |
| parent | 66a68a4329ce199f25184ba8b2d98b4679e7ddae (diff) | |
Renaming allow_patvar flag of intern_gen into pattern_mode.
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
Diffstat (limited to 'pretyping/typeclasses_errors.mli')
0 files changed, 0 insertions, 0 deletions