diff options
| author | Brian Campbell | 2018-08-16 17:32:32 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-08-16 17:32:42 +0100 |
| commit | 18900d3c0da37c4dc7079749f84517fb7456e551 (patch) | |
| tree | 08e373e6b2bf301f36cdb302a01f4bad942f1166 /src/bytecode_util.ml | |
| parent | eee4d26e53a5e33cdb71e9a338154e2dbf18830c (diff) | |
Add the type an expression was checked against to tannots, and use for Coq
Tweak extra Coq files to match.
Tweak early return rewrite to use declared return type, which can always
be put into an E_cast.
Diffstat (limited to 'src/bytecode_util.ml')
0 files changed, 0 insertions, 0 deletions