From cf9524560f6174cad6632136fa46a2dd43dbd91d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Mar 2016 16:40:04 +0100
Subject: [PATCH] Solve Import cofe_solver situation.

Requires should always be at the top of a file, Imports can be inside
of submodules.

It is strange that a Require in a submodule is allowed and then triggers
an error when using the whole module. This may be a Coq bug.
---
 program_logic/model.v | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/program_logic/model.v b/program_logic/model.v
index 08960cef5..8c8a0aea5 100644
--- a/program_logic/model.v
+++ b/program_logic/model.v
@@ -1,9 +1,6 @@
 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.
+From iris.algebra Require cofe_solver.
 
 (* The Iris program logic is parametrized by a locally contractive functor
 from the category of COFEs to the category of CMRAs, which is instantiated
@@ -36,6 +33,7 @@ Parameter iProp_unfold_fold: ∀ {Λ Σ} (P : iPreProp Λ Σ),
 End iProp_solution_sig.
 
 Module Export iProp_solution : iProp_solution_sig.
+Import cofe_solver.
 Definition iProp_result (Λ : language) (Σ : iFunctor) :
   solution (uPredCF (resRF Λ (▶ ∙) Σ)) := solver.result _.
 
-- 
GitLab