From 0e0c64bf93f33044d299bfd5456d9a6b00992a0d Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Wed, 1 Jul 2020 20:09:15 +0100
Subject: Improve (?) automation.

---
 src/translation/HTLgenspec.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/translation/HTLgenspec.v')

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. *)
-- 
cgit