From b51b7a70fce3eb6a63e2cf0072c93b11354fd6e0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= <pierre-marie.pedrot@inria.fr>
Date: Tue, 5 Feb 2019 13:30:59 +0100
Subject: [PATCH] Set the Ltac backtrace option in tests.

This is a change enabling backward compatibility.
---
 tests/heap_lang.v         | 1 +
 tests/proofmode.v         | 1 +
 tests/proofmode_iris.v    | 1 +
 tests/proofmode_monpred.v | 1 +
 4 files changed, 4 insertions(+)

diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 0ab4a6b4d..a738ffb97 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,6 +2,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
 From iris.heap_lang Require Import lang adequacy proofmode notation.
 (* Import lang *again*. This used to break notation. *)
 From iris.heap_lang Require Import lang.
+Set Ltac Backtrace.
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index c4566b7b4..7fd712ccb 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,4 +1,5 @@
 From iris.proofmode Require Import tactics intro_patterns.
+Set Ltac Backtrace.
 Set Default Proof Using "Type".
 
 Section tests.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index 0beb0b2d3..545967539 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,6 +1,7 @@
 From iris.proofmode Require Import tactics monpred.
 From iris.base_logic Require Import base_logic.
 From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants.
+Set Ltac Backtrace.
 
 Section base_logic_tests.
   Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index c683a11a7..a88a79168 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,4 +1,5 @@
 From iris.proofmode Require Import tactics monpred.
+Set Ltac Backtrace.
 
 Section tests.
   Context {I : biIndex} {PROP : sbi}.
-- 
GitLab