diff options
| author | Hugo Herbelin | 2014-12-15 16:48:32 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-15 19:18:42 +0100 |
| commit | c73f114a46d50ab7c22218db0e80d5da96a824e4 (patch) | |
| tree | bb25f7c078face1ef8a9b228f234773b3d1243b1 /kernel | |
| parent | a87dd193cb6a31ba528626e34a1bbb9b58c14f2e (diff) | |
Failing on unbound notation variable in notation level modifiers
+ consequences of this check on the standard library (moved the no-op
in Notation modifiers to what there were supposed to do; these are
anyway local notations, so compatibility is safe - please AS or PL,
amend if needed).
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions