Commit 56f80319 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Break a depedency.

parent bce1a24c
From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
......
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