From b043f3a345b624534b8491647b1d3a01a615afe6 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Wed, 23 May 2018 16:00:08 +0200 Subject: [PATCH] don't export derived, that leads to uPred being the wrong module --- theories/base_logic/lib/fractional.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v index 179eac0fc..104146e53 100644 --- a/theories/base_logic/lib/fractional.v +++ b/theories/base_logic/lib/fractional.v @@ -1,5 +1,5 @@ From stdpp Require Import gmap gmultiset. -From iris.base_logic Require Export derived. +From iris.base_logic Require Export base_logic. From iris.base_logic Require Import big_op. From iris.proofmode Require Import classes class_instances. Set Default Proof Using "Type". -- GitLab