diff options
| author | Gaëtan Gilbert | 2019-11-19 14:28:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-11-26 11:28:55 +0100 |
| commit | 1db8720bf624c202dcc4f1eecdcde803fed4efc2 (patch) | |
| tree | 3c762f209ff0f00aa11120488f9e6cf5a65a1118 /configure.ml | |
| parent | a5d124dd7c3d43a5ead81cfac30c7d1448002d56 (diff) | |
indTyping: error instead of anomaly for ill-formed template
and do not run template_candidate in the upper layers when the
template attribute is given.
This means we can use an over-approximation in the upper layer
implementation of template_candidate (returning false even in cases
which the kernel may accept) if we ever want to.
Diffstat (limited to 'configure.ml')
0 files changed, 0 insertions, 0 deletions