diff options
| author | Pierre-Marie Pédrot | 2020-09-03 14:28:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-13 19:43:48 +0200 |
| commit | 674dcda367d9ed43f3b0cc8264a0ef10bc7fd751 (patch) | |
| tree | 9fae7950d3c560032688faf98e0aae6d2ee31c8d /dev | |
| parent | e1a8da8b83aa3ae96ac05c2bc6606aa0719aa64f (diff) | |
Statically ensure that only polymophic hint terms come with a context.
It is the duty of the caller to properly declare monomorphic global
constraints when creating a non-globref hint. All callers were already
abiding by this convention.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions