Closed andrew-appel closed 1 year ago
The match in Ltac floyd.forward.check_parameter_vals should be a lazymatch, otherwise the fail 4 goes to the wrong place.
match
lazymatch
fail 4
This is not quite correct; changing a match to a lazymatch breaks some test cases.
The
match
in Ltac floyd.forward.check_parameter_vals should be alazymatch
, otherwise thefail 4
goes to the wrong place.