Prophecy variables

See merge request FP/iris-coq!173

Support multiple steps in `PureExec`.

See merge request FP/iris-coq!179

Snapshot will re-appear in iris-examples eventually

Marianna Rapoport authored Jul 23, 2018 and Ralf Jung committed Oct 05, 2018

- Removing admitted prophecy spec and making prophecy-related examples (coin-flip and atomic-pair-snapshot) work with the new prophecy support in heap_lang
- Adjusting heap_lang tactics for automation of substitution, closedness, etc. to support prophecy syntax
- Adding notation for prophecy syntax

Marianna Rapoport authored Jul 17, 2018 and Ralf Jung committed Oct 05, 2018

- Removing head of list of observations after each reduction step in definition of wp
- Adding support for observations to state_interp and world
- Applying Ralf's suggestions to previous commit (e.g. replacing /\ and -> with unicode characters)