summaryrefslogtreecommitdiff
path: root/language/bytecode.ott
diff options
context:
space:
mode:
authorBrian Campbell2018-08-16 17:32:32 +0100
committerBrian Campbell2018-08-16 17:32:42 +0100
commit18900d3c0da37c4dc7079749f84517fb7456e551 (patch)
tree08e373e6b2bf301f36cdb302a01f4bad942f1166 /language/bytecode.ott
parenteee4d26e53a5e33cdb71e9a338154e2dbf18830c (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 'language/bytecode.ott')
0 files changed, 0 insertions, 0 deletions