From 7c00020b174fbe48454a8cfc9e6fd87a3bd47f3b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Feb 2018 02:27:17 +0100
Subject: [PATCH] Kill dependency of `base_logic` on `proofmode` to speed up
 compilation.

---
 theories/base_logic/base_logic.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 5a947722e..4aecb160d 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -1,6 +1,5 @@
 From iris.base_logic Require Export derived.
 From iris.bi Require Export bi.
-From iris.proofmode Require Import tactics.
 From iris.algebra Require Import proofmode_classes.
 Set Default Proof Using "Type".
 
-- 
GitLab