diff --git a/coq/ra/escrows.v b/coq/ra/escrows.v index 2d622c6d3d32048568e0db153ee3f5b5d05edb71..b180a9b8a5c287f062847d0c3a8f8eb3be5cfaed 100644 --- a/coq/ra/escrows.v +++ b/coq/ra/escrows.v @@ -3,8 +3,9 @@ From iris.algebra Require Import agree. From iris.prelude Require Import gmap. From iris.proofmode Require Import tactics. -From ra Require Import views viewpred proofmode abs_view. +From ra Require Import views viewpred proofmode. From ra.base Require Import ghosts. +From ra Require Export abs_view. Definition escrowN : namespace := nroot .@ "escrow".