From 3bf046f2cf5e8cb8e3fa7288c15ddb2674a239b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 Jun 2019 15:24:00 +0200
Subject: [PATCH] fix ref tests for Coq 8.10+

---
 tests/solve_ndisj.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/solve_ndisj.v b/tests/solve_ndisj.v
index 3ed8e1f9..7a58ba3a 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.
-- 
GitLab