diff options
| author | James Pollard <james@pollard.dev> | 2020-07-01 20:09:15 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-07-01 20:09:15 +0100 |
| commit | 0e0c64bf93f33044d299bfd5456d9a6b00992a0d (patch) | |
| tree | 59289787f1e1520f39e666583207b5c3ff60322a /src/translation/HTLgenspec.v | |
| parent | 24b07d3b719072482f609954f584232534ed93eb (diff) | |
| download | vericert-0e0c64bf93f33044d299bfd5456d9a6b00992a0d.tar.gz vericert-0e0c64bf93f33044d299bfd5456d9a6b00992a0d.zip | |
Improve (?) automation.
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index a78256b..0cdecba 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -426,7 +426,7 @@ Proof. destruct (0 <=? RTL.fn_stacksize f) eqn:STACK_BOUND_LOW; destruct (RTL.fn_stacksize f <? Integers.Ptrofs.modulus) eqn:STACK_BOUND_HIGH; destruct (RTL.fn_stacksize f mod 4 =? 0) eqn:STACK_ALIGN; - simplify; + crush; monadInv Heqr. (* TODO: We should be able to fold this into the automation. *) |