Commit 3b0457d4 authored by Ralf Jung's avatar Ralf Jung

add another printing hint for normalization

parent f2e41316
Pipeline #24319 passed with stage
in 16 minutes and 7 seconds
From iris.proofmode Require Import tactics monpred.
From iris.base_logic.lib Require Import invariants.
Set Ltac Backtrace. (* FIXME: remove once we drop Coq 8.9 *)
Unset Printing Use Implicit Types. (* FIXME: remove once all supported Coq versions ship with <https://github.com/coq/coq/pull/11261>. *)
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