From c2a8bce04fe07ded69ace301f414b49038b30808 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 21 Mar 2018 14:13:48 +0100
Subject: [PATCH] move general BI things using the proofmode down into lib/
---
_CoqProject | 4 ++--
theories/bi/{ => lib}/counter_examples.v | 0
theories/bi/{ => lib}/fixpoint.v | 0
3 files changed, 2 insertions(+), 2 deletions(-)
rename theories/bi/{ => lib}/counter_examples.v (100%)
rename theories/bi/{ => lib}/fixpoint.v (100%)
diff --git a/_CoqProject b/_CoqProject
index 50d473944..fdfda5bfd 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -33,10 +33,10 @@ theories/bi/big_op.v
theories/bi/updates.v
theories/bi/bi.v
theories/bi/tactics.v
-theories/bi/counter_examples.v
-theories/bi/fixpoint.v
theories/bi/monpred.v
theories/bi/embedding.v
+theories/bi/lib/counter_examples.v
+theories/bi/lib/fixpoint.v
theories/bi/lib/fractional.v
theories/bi/lib/atomic.v
theories/bi/lib/core.v
diff --git a/theories/bi/counter_examples.v b/theories/bi/lib/counter_examples.v
similarity index 100%
rename from theories/bi/counter_examples.v
rename to theories/bi/lib/counter_examples.v
diff --git a/theories/bi/fixpoint.v b/theories/bi/lib/fixpoint.v
similarity index 100%
rename from theories/bi/fixpoint.v
rename to theories/bi/lib/fixpoint.v
--
GitLab