Commit eb921edd authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'disable-ltac-backtrace' into 'master'

Set the Ltac backtrace option in tests.

See merge request iris/iris!213
parents 5fd7dae1 b51b7a70
Pipeline #14409 passed with stage
in 11 minutes and 31 seconds
...@@ -2,6 +2,7 @@ From iris.program_logic Require Export weakestpre total_weakestpre. ...@@ -2,6 +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 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 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.
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.
Set Ltac Backtrace.
Section tests. Section tests.
Context {I : biIndex} {PROP : sbi}. Context {I : biIndex} {PROP : sbi}.
......
Supports Markdown
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