From a97115311c6c40c7a45243a2d4eb6d3d2294a69e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Mar 2016 10:28:09 +0100
Subject: [PATCH] we would like to import cofe_solver only within the (sealed)
 module iProp_solution...

...but it does not work. Hu?
---
 program_logic/model.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/program_logic/model.v b/program_logic/model.v
index ce2cf3f1b..08960cef5 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,5 +1,8 @@
 From iris.algebra Require Export upred.
 From iris.program_logic Require Export resources.
+(* We'd prefer to only import this in the sealed module, to make sure it does
+   not "escape". However, for some reason, that breaks importing model.v
+   elsewhere. *)
 From iris.algebra Require Import cofe_solver.
 
 (* The Iris program logic is parametrized by a locally contractive functor
-- 
GitLab