Commit cf952456 authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent 2e0993b1
Pipeline #367 passed with stage
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 _.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment