Main paper (version 2020-12-26)

paper-2020-12-26-a0142032

Refactor oracle (and its props) out into a separate module

Main paper (version 2020-12-25)

paper-2020-12-25-15d7817f

Build with -shell-escape in the CI as well

Main paper (version 2020-12-24)

paper-2020-12-24-c25f4e7d

Merge cbd1ace4699e478646a86835827b590219e467e2 into e680fb572a6e41f7d…

Main paper (version 2020-12-24)

Fix github CI action (#5)

Hopefully fix the Github CI action for building the PDF

Main paper (version 2020-12-08)

paper-2020-12-08-e60865d0

Add references to papers on CoqHammer and Meta-F*

Main paper (version 2020-12-08)

paper-2020-12-08-3d51b124

Minor stylistic fixes

Main paper (version 2020-12-08)

paper-2020-12-08-63f47c81

Minor text style fixes

Main paper (version 2020-11-13)

paper-2020-11-13-ed9f175f

Lol, forgot lambda body term

Main paper (version 2020-11-11)

Remove the now-duplicated bullet on implementability

And it's not a metatheoretical property anyway.

Main paper (version 2020-11-09)

Start working on weakening for types

Not sure if that's the right way to go, but I don't really see any other
way of going forward with the dependency of types on contexts.