diff options
| author | Hugo Herbelin | 2018-10-31 20:29:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 11d293e692adc801545f714d3851fa7a4fef8266 (patch) | |
| tree | 9d016fc95f09d26dd1db2a8af63967e8ce0b6fc6 /dev | |
| parent | 4b02fbd92ec47f1477db71425d2627898019cd5d (diff) | |
Notation.ml: Moving code about binding scopes to coercion classes earlier.
We shall need it for changing the semantics of type_scope.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions