From 65296d1a832dab09c58d21c0955c91738a7cbff3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 2 Jul 2016 12:00:22 +0200
Subject: [PATCH] Ensure that solve_ndisj "solves", it either succeeds or
 fails.

---
 program_logic/namespaces.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index ac5d73aba..0783c7564 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -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_r : ndisj.
 
-Ltac solve_ndisj := eauto with ndisj.
+Ltac solve_ndisj := solve [eauto with ndisj].
-- 
GitLab