Commit b51b7a70 authored by Pierre-Marie Pédrot's avatar Pierre-Marie Pédrot

Set the Ltac backtrace option in tests.

This is a change enabling backward compatibility.
parent 5fd7dae1
......@@ -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.
......
From iris.proofmode Require Import tactics intro_patterns.
Set Ltac Backtrace.
Set Default Proof Using "Type".
Section tests.
......
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}.
......
From iris.proofmode Require Import tactics monpred.
Set Ltac Backtrace.
Section tests.
Context {I : biIndex} {PROP : sbi}.
......
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