Commit f2e41316 authored by Ralf Jung's avatar Ralf Jung

note that 'Set Ltac Backtrace' is just a compat hack

parent 564b7d5c
...@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics. ...@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From iris.program_logic Require Export atomic. From iris.program_logic Require Export atomic.
From iris.heap_lang Require Export lifting notation. From iris.heap_lang Require Export lifting notation.
From iris.heap_lang Require Import proofmode notation atomic_heap. 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". Set Default Proof Using "Type".
Section tests. Section tests.
......
...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre. ...@@ -2,7 +2,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre.
From iris.heap_lang Require Import lang adequacy proofmode notation. From iris.heap_lang Require Import lang adequacy proofmode notation.
(* Import lang *again*. This used to break notation. *) (* Import lang *again*. This used to break notation. *)
From iris.heap_lang Require Import lang. 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". Set Default Proof Using "Type".
Section tests. Section tests.
......
From iris.proofmode Require Import tactics intro_patterns. 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". Set Default Proof Using "Type".
Section tests. Section tests.
......
From iris.proofmode Require Import tactics monpred. From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic. From iris.base_logic Require Import base_logic.
From iris.base_logic.lib Require Import invariants cancelable_invariants na_invariants. 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. Section base_logic_tests.
Context {M : ucmraT}. Context {M : ucmraT}.
......
From iris.proofmode Require Import tactics monpred. From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Set Ltac Backtrace. Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Section tests. Section tests.
Context {I : biIndex} {PROP : sbi}. Context {I : biIndex} {PROP : sbi}.
......
From iris.proofmode Require Import tactics . From iris.proofmode Require Import tactics .
From iris.si_logic Require Import bi. 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. Section si_logic_tests.
Implicit Types P Q R : siProp. Implicit Types P Q R : siProp.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment