This P.R. implements the suggestion in issue #625. It's an experiment, as in some cases it breaks existing VST proofs at forward_if and related tactics. The changes required in those proofs are generally positive (simplifies proof scripts). See further discussion at #625. closes #625
This P.R. implements the suggestion in issue #625. It's an experiment, as in some cases it breaks existing VST proofs at
forward_ifand related tactics. The changes required in those proofs are generally positive (simplifies proof scripts). See further discussion at #625. closes #625Incidentally and unrelated: closes #660