Commit 65296d1a authored by Robbert Krebbers's avatar Robbert Krebbers

Ensure that solve_ndisj "solves", it either succeeds or fails.

parent 2bc4df02
...@@ -68,4 +68,4 @@ Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj. ...@@ -68,4 +68,4 @@ Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l : ndisj. Hint Resolve ndot_preserve_disjoint_l : ndisj.
Hint Resolve ndot_preserve_disjoint_r : ndisj. Hint Resolve ndot_preserve_disjoint_r : ndisj.
Ltac solve_ndisj := eauto with 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