From 114b46c7a267a5aeba58431d57e612d4761f9dac Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Tue, 2 Feb 2016 16:14:26 +0100 Subject: [PATCH] reduce imports of language.v --- iris/language.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/iris/language.v b/iris/language.v index afa23eb9c..1a4bc01b2 100644 --- a/iris/language.v +++ b/iris/language.v @@ -1,4 +1,4 @@ -Require Export modures.cmra. +Require Export modures.cofe. Structure language := Language { expr : Type; -- GitLab