diff options
| author | Hugo Herbelin | 2018-10-31 20:32:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 0336e86ea5ef63a587aae695adeeb4607346c337 (patch) | |
| tree | d3fef8cfa533a9965b992aeed8b5f79dc8422374 /dev | |
| parent | 11d293e692adc801545f714d3851fa7a4fef8266 (diff) | |
Giving to type_scope a softer role in printing.
Namely, it does not explicitly open a scope, but we remember that we
don't need the %type delimiter when in type position.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions