Skip to content
Snippets Groups Projects
Commit a5ee0c16 authored by Ralf Jung's avatar Ralf Jung
Browse files

move coPset-generic hint to coPset.v

parent 1f223f8f
No related branches found
No related tags found
No related merge requests found
......@@ -159,6 +159,7 @@ Instance coPset_singleton : Singleton positive coPset := λ p,
Instance coPset_elem_of : ElemOf positive coPset := λ p X, e_of p (`X).
Instance coPset_empty : Empty coPset := coPLeaf false I.
Instance coPset_top : Top coPset := coPLeaf true I.
Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
Instance coPset_union : Union coPset := λ X Y,
let (t1,Ht1) := X in let (t2,Ht2) := Y in
(t1 t2) coPset_union_wf _ _ Ht1 Ht2.
......
......@@ -85,10 +85,6 @@ Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
Hint Resolve nclose_subseteq' | 100 : ndisj.
(** Put this hint in [core] so that only only [solve_ndisj], but also [done] and
friends, can solve trivial goals of the form [E ⊆ ⊤] that occur often. *)
Hint Resolve (top_subseteq (A:=positive) (C:=coPset)) : core.
(** Rules for goals of the form [_ ## _] *)
(** The base rule that we want to ultimately get down to. *)
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment