Skip to content

I
Iris
Commit 2472f932 authored by Ralf Jung's avatar Ralf Jung
Browse files
Options

make ndisj hints look through definitions to unfold more stuff

parent 1c548c0c
Pipeline #3408 passed with stage
    in 17 minutes and 49 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 2 additions and 2 deletions
    theories/base_logic/lib/namespaces.v
    View file @ 2472f932
    ......@@ -88,8 +88,8 @@ of the forms:
    - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
    Hint Resolve ndisj_subseteq_difference : ndisj.
    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 ndot_preserve_disjoint_l : ndisj.
    Hint Extern 1 (_ ⊥ _) => apply ndot_preserve_disjoint_r : ndisj.
    Hint Extern 1 (_ ⊆ _) => apply nclose_subseteq' : ndisj.
    Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
    Hint Resolve ndisj_difference_l : 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