From 72f4ea9ee6503b05fba0f7d38117aac40e3f14a0 Mon Sep 17 00:00:00 2001 From: Hai Dang <haidang@mpi-sws.org> Date: Fri, 10 Feb 2017 15:47:27 +0100 Subject: [PATCH] fix absView Require Export --- coq/ra/escrows.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/coq/ra/escrows.v b/coq/ra/escrows.v index 2d622c6d..b180a9b8 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". -- GitLab