Fix hint locality for 8.17

inQWIRE · Jan 21, 2025 · 380837c · 380837c
1 parent d23b369
commit 380837c
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/CoreData/Proportional.v b/src/CoreData/Proportional.v
@@ -322,12 +322,16 @@ Create HintDb zx_prop_by_db discriminated.
   colorswap_prop_by_compat : zx_prop_by_db.
 
 (* For concrete examples with bad sizes *)
+#[export]
 Hint Extern 0 (?x ⟷ ?y ∝[?c] ?x ⟷ ?z) =>
   apply (compose_prop_by_compat_r x y z) : zx_prop_by_db.
+#[export]
 Hint Extern 0 (?x ⟷ ?y ∝[?c] ?z ⟷ ?y) =>
   apply (compose_prop_by_compat_l x z y) : zx_prop_by_db.
+#[export]
 Hint Extern 0 (?x ↕ ?y ∝[?c] ?x ↕ ?z) =>
   apply (stack_prop_by_compat_r x y z) : zx_prop_by_db.
+#[export]
 Hint Extern 0 (?x ↕ ?y ∝[?c] ?z ↕ ?y) =>
   apply (stack_prop_by_compat_l x z y) : zx_prop_by_db.