From c36ae2bd641910fe58995ee4cf32c5073fb3fad2 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 10 Dec 2020 20:09:15 +0100 Subject: [PATCH] remove unused import of hoare module --- theories/lang/races.v | 1 - 1 file changed, 1 deletion(-) diff --git a/theories/lang/races.v b/theories/lang/races.v index 35044a02..9c923d16 100644 --- a/theories/lang/races.v +++ b/theories/lang/races.v @@ -1,5 +1,4 @@ From stdpp Require Import gmap. -From iris.program_logic Require Export hoare. From iris.program_logic Require Import adequacy. From lrust.lang Require Import tactics. Set Default Proof Using "Type". -- GitLab