Commit f133c8cd authored by Robbert Krebbers's avatar Robbert Krebbers

Move derived `auth` algebra stuff in `lib` folder.

parent 9a3439f5
......@@ -17,8 +17,6 @@ theories/algebra/big_op.v
theories/algebra/cmra_big_op.v
theories/algebra/sts.v
theories/algebra/auth.v
theories/algebra/frac_auth.v
theories/algebra/excl_auth.v
theories/algebra/gmap.v
theories/algebra/ofe.v
theories/algebra/base.v
......@@ -40,7 +38,9 @@ theories/algebra/deprecated.v
theories/algebra/proofmode_classes.v
theories/algebra/ufrac.v
theories/algebra/namespace_map.v
theories/algebra/ufrac_auth.v
theories/algebra/lib/excl_auth.v
theories/algebra/lib/frac_auth.v
theories/algebra/lib/ufrac_auth.v
theories/bi/notation.v
theories/bi/interface.v
theories/bi/derived_connectives.v
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl_auth gmap agree.
From iris.algebra Require Import lib.excl_auth gmap agree.
From iris.base_logic.lib Require Export invariants.
Set Default Proof Using "Type".
Import uPred.
......
From iris.proofmode Require Import tactics.
From iris.algebra Require Import frac_auth auth.
From iris.algebra Require Import lib.frac_auth auth.
From iris.base_logic.lib Require Export invariants.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang.
......
From iris.proofmode Require Import tactics classes.
From iris.algebra Require Import excl_auth.
From iris.algebra Require Import lib.excl_auth.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
......
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