we would like to import cofe_solver only within the (sealed) module iProp_solution...

...but it does not work. Hu?

we would like to import cofe_solver only within the (sealed) module iProp_solution...
...but it does not work. Hu?
a9711531 · Ralf Jung · ab77927c · a9711531
Commit a9711531 authored Mar 17, 2016 by Ralf Jung
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

program_logic/model.v program_logic/model.v +3 -0

No files found.
--- a/program_logic/model.v
+++ b/program_logic/model.v
 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