Commit c1be91f7 authored by Ralf Jung's avatar Ralf Jung

move fractional.v to new lib/ folder

parent a0ac556c
...@@ -32,11 +32,11 @@ theories/bi/big_op.v ...@@ -32,11 +32,11 @@ theories/bi/big_op.v
theories/bi/updates.v theories/bi/updates.v
theories/bi/bi.v theories/bi/bi.v
theories/bi/tactics.v theories/bi/tactics.v
theories/bi/fractional.v
theories/bi/counter_examples.v theories/bi/counter_examples.v
theories/bi/fixpoint.v theories/bi/fixpoint.v
theories/bi/monpred.v theories/bi/monpred.v
theories/bi/embedding.v theories/bi/embedding.v
theories/bi/lib/fractional.v
theories/base_logic/upred.v theories/base_logic/upred.v
theories/base_logic/derived.v theories/base_logic/derived.v
theories/base_logic/base_logic.v theories/base_logic/base_logic.v
......
From iris.base_logic.lib Require Export invariants. From iris.base_logic.lib Require Export invariants.
From iris.bi Require Import fractional. From iris.bi.lib Require Import fractional.
From iris.algebra Require Export frac. From iris.algebra Require Export frac.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
From iris.algebra Require Import auth gmap frac agree. From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic.lib Require Export own. From iris.base_logic.lib Require Export own.
From iris.bi Require Import fractional. From iris.bi.lib Require Import fractional.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import uPred. Import uPred.
......
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