From c9c2343a2a2260ae011f88e5c4f847eb52e0569a Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 21 Nov 2019 13:31:06 +0100 Subject: [PATCH] reorder imports for Coq master compat --- theories/heap_lang/proph_erasure.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/heap_lang/proph_erasure.v b/theories/heap_lang/proph_erasure.v index 6f3f155c3..547cb57f4 100644 --- a/theories/heap_lang/proph_erasure.v +++ b/theories/heap_lang/proph_erasure.v @@ -1,5 +1,5 @@ -From iris.heap_lang Require Export lang notation tactics. From iris.program_logic Require Export adequacy. +From iris.heap_lang Require Export lang notation tactics. (** This file contains the proof that prophecies can be safely erased from programs. We erase a program by replacing prophecy identifiers -- GitLab