diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 3ed8e1f91825fc0494e8f2d04cf09879efd2ba27..7a58ba3acafebc142888767f88d952357e1468b1 100644
--- a/tests/solve_ndisj.v
+++ b/tests/solve_ndisj.v
@@ -1,5 +1,7 @@
 From stdpp Require Import namespaces strings.
 
+Set Ltac Backtrace.
+
 Lemma test1 (N1 N2 : namespace) :
   N1 ## N2 → ↑N1 ⊆@{coPset} ⊤ ∖ ↑N2.
 Proof. solve_ndisj. Qed.