Commit 2f67cbdc authored by Robbert Krebbers's avatar Robbert Krebbers

Move upred to algebra as it is not tied to the Iris logic.

parent 66f61d49
......@@ -49,7 +49,7 @@ algebra/agree.v
algebra/excl.v
algebra/iprod.v
algebra/functor.v
program_logic/upred.v
algebra/upred.v
program_logic/model.v
program_logic/adequacy.v
program_logic/hoare_lifting.v
......
(** This file is essentially a bunch of testcases. *)
Require Import program_logic.upred program_logic.ownership.
Require Import program_logic.ownership.
Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang uPred notations.
......
Require Export program_logic.upred program_logic.resources.
Require Export algebra.upred program_logic.resources.
Require Import algebra.cofe_solver.
(* The Iris program logic is parametrized by a functor from the category of
......
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