Commit b043f3a3 authored by Ralf Jung's avatar Ralf Jung

don't export derived, that leads to uPred being the wrong module

parent 4fc7ee79
From stdpp Require Import gmap gmultiset. 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.base_logic Require Import big_op.
From iris.proofmode Require Import classes class_instances. From iris.proofmode Require Import classes class_instances.
Set Default Proof Using "Type". Set Default Proof Using "Type".
......
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