• Robbert Krebbers's avatar
    Random stuff that breaks everything: · 5fb2e503
    Robbert Krebbers authored
    - Add support for fst/snd/pair to the vcg_gen + reified expressions for non-monadic expressions.
    - Make `cloc_to_val` locked so that it will _never_ be unfolded.
    - Support locations + offsets in the reified language.
    - Drop `vcg_compute`, it left huge thunks of computation, making some things super slow. Just use `simpl` with appropriate `Arguments` instead.
    5fb2e503
translation.v 21.8 KB