From 23cd0c7d586dfc86412e7ec9b64413c7d3d532b6 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 16 Dec 2016 14:40:28 +0100 Subject: [PATCH] fix assigning priority to ndisj hint --- theories/base_logic/lib/namespaces.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/base_logic/lib/namespaces.v b/theories/base_logic/lib/namespaces.v index 549ecf193..58819d812 100644 --- a/theories/base_logic/lib/namespaces.v +++ b/theories/base_logic/lib/namespaces.v @@ -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]. -- GitLab