diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v index 66a18ed735bef035e1628a9146882d8b64bed92a..6d872ce5353679fab50daaf00627621148023e70 100644 --- a/theories/examples/map_reduce.v +++ b/theories/examples/map_reduce.v @@ -1,7 +1,7 @@ From actris.channel Require Import proto_channel proofmode. From iris.heap_lang Require Import proofmode notation. From actris.utils Require Import llist compare contribution group. -From actris.examples Require Import map sort_fg_client. +From actris.examples Require Import map sort_fg. From iris.algebra Require Import gmultiset. (** Functional version of map reduce (aka the specification) *)