From f2e41316a791f1c04909bda1cf5a82bb596ab0af Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 Feb 2020 08:51:58 +0100
Subject: [PATCH] note that 'Set Ltac Backtrace' is just a compat hack
---
tests/atomic.v | 2 +-
tests/heap_lang.v | 2 +-
tests/proofmode.v | 2 +-
tests/proofmode_iris.v | 2 +-
tests/proofmode_monpred.v | 2 +-
tests/proofmode_siprop.v | 2 +-
6 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/tests/atomic.v b/tests/atomic.v
index 62e5e2334..afc6e55bd 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation atomic_heap.
-Set Ltac Backtrace.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Set Default Proof Using "Type".
Section tests.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f353c853d..b0bb09df6 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -2,7 +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 Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Set Default Proof Using "Type".
Section tests.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 6057efb1c..735c423a3 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1,5 +1,5 @@
From iris.proofmode Require Import tactics intro_patterns.
-Set Ltac Backtrace.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Set Default Proof Using "Type".
Section tests.
diff --git a/tests/proofmode_iris.v b/tests/proofmode_iris.v
index c2998995f..3bfbc2ee5 100644
--- a/tests/proofmode_iris.v
+++ b/tests/proofmode_iris.v
@@ -1,7 +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.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Section base_logic_tests.
Context {M : ucmraT}.
diff --git a/tests/proofmode_monpred.v b/tests/proofmode_monpred.v
index 320355c44..b76927b8b 100644
--- a/tests/proofmode_monpred.v
+++ b/tests/proofmode_monpred.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants.
-Set Ltac Backtrace.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Section tests.
Context {I : biIndex} {PROP : sbi}.
diff --git a/tests/proofmode_siprop.v b/tests/proofmode_siprop.v
index d9dc2c4e8..34a032198 100644
--- a/tests/proofmode_siprop.v
+++ b/tests/proofmode_siprop.v
@@ -1,6 +1,6 @@
From iris.proofmode Require Import tactics .
From iris.si_logic Require Import bi.
-Set Ltac Backtrace.
+Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Section si_logic_tests.
Implicit Types P Q R : siProp.
--
GitLab