Skip to content

I
Iris
Commit 23cd0c7d authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

fix assigning priority to ndisj hint

parent b1fa82f0
Hide whitespace changes
Inline Side-by-side
Showing with 1 addition and 1 deletion
theories/base_logic/lib/namespaces.v
View file @ 23cd0c7d
......@@ -91,7 +91,7 @@ Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj.
Hint Extern 1 (_ ⊆ _) => apply nclose_subseteq' : ndisj.
Hint Resolve 100 namespace_subseteq_difference_l : ndisj.
Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
Hint Resolve ndisj_difference_l : ndisj.
Ltac solve_ndisj := solve [eauto with ndisj].
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment