diff options
| author | Thomas Bauereiss | 2020-03-22 18:21:57 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2020-04-21 01:04:21 +0100 |
| commit | 4b6ffe96896f56d538dc9115c1d1b04156ab34a5 (patch) | |
| tree | 1c3dc102e5216986607cddd5ec8f124133a8c57e /src/splice.ml | |
| parent | 3d895704db4689f832180782ab30f1805804e2b3 (diff) | |
Be more careful about type annotations in rewrites to Lem
In particular, don't add annotations for types with existentially
quantified variables that only occur in constraints, not in the type,
e.g. {'i1 'i2, 'i1 == div('i2, 8). int('i1)}. These seem to confuse the
type checker when pulled out into the source AST.
Diffstat (limited to 'src/splice.ml')
0 files changed, 0 insertions, 0 deletions