From 7dec931b3ce0674c093a325275976aac96e9c8e6 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 28 Mar 2017 01:07:55 +0200 Subject: [PATCH] Enable solve_ndisj to handle unions on the LHS. --- theories/base_logic/lib/namespaces.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v index c4eb25c6..cb8dde63 100644 --- a/theories/base_logic/lib/namespaces.v +++ b/theories/base_logic/lib/namespaces.v @@ -90,10 +90,11 @@ of the forms: Create HintDb ndisj. Hint Resolve ndisj_subseteq_difference : ndisj. Hint Extern 0 (_ ⊥ _) => apply ndot_ne_disjoint; congruence : ndisj. -Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r - nclose_subseteq' ndisj_difference_l : ndisj. +Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj. +Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj. Hint Resolve namespace_subseteq_difference_l | 100 : ndisj. Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj. +Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj. Ltac solve_ndisj := repeat match goal with -- GitLab