-
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