From c1be91f7834799d780d0b1c19b24a1f58b7ebd8e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 15 Feb 2018 17:44:31 +0100
Subject: [PATCH] move fractional.v to new lib/ folder
---
_CoqProject | 2 +-
theories/base_logic/lib/cancelable_invariants.v | 2 +-
theories/base_logic/lib/gen_heap.v | 2 +-
theories/bi/{ => lib}/fractional.v | 0
4 files changed, 3 insertions(+), 3 deletions(-)
rename theories/bi/{ => lib}/fractional.v (100%)
diff --git a/_CoqProject b/_CoqProject
index d7abc183f..dc79c329b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -32,11 +32,11 @@ theories/bi/big_op.v
theories/bi/updates.v
theories/bi/bi.v
theories/bi/tactics.v
-theories/bi/fractional.v
theories/bi/counter_examples.v
theories/bi/fixpoint.v
theories/bi/monpred.v
theories/bi/embedding.v
+theories/bi/lib/fractional.v
theories/base_logic/upred.v
theories/base_logic/derived.v
theories/base_logic/base_logic.v
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index 9d5f84d7f..fa21aad63 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -1,5 +1,5 @@
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.proofmode Require Import tactics.
Set Default Proof Using "Type".
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index c37e3b678..3550f0cd7 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -1,6 +1,6 @@
From iris.algebra Require Import auth gmap frac agree.
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.
Set Default Proof Using "Type".
Import uPred.
diff --git a/theories/bi/fractional.v b/theories/bi/lib/fractional.v
similarity index 100%
rename from theories/bi/fractional.v
rename to theories/bi/lib/fractional.v
--
GitLab