unfold aligned_to and Z.divide before lia

06460813 · Michael Sammler · 02c3ff05 · 06460813
Commit 06460813 authored Jun 10, 2021 by Michael Sammler
--- a/theories/typing/automation/solvers.v
+++ b/theories/typing/automation/solvers.v
@@ -8,6 +8,8 @@ Proof. done. Qed.

 Ltac unfold_common_defs :=
  unfold
+  (* Unfold [aligned_to] and [Z.divide] as lia can work with the underlying multiplication. *)
+    aligned_to, Z.divide,
  (* Unfold [addr] since [lia] may get stuck due to [addr]/[Z] mismatches. *)
    addr,
  (* Layout *)