Commit ad9aa6eb authored by Ralf Jung's avatar Ralf Jung
Browse files

move upred.v into the right folder

parent cf888992
...@@ -41,13 +41,13 @@ algebra/cmra_tactics.v ...@@ -41,13 +41,13 @@ algebra/cmra_tactics.v
algebra/sts.v algebra/sts.v
algebra/auth.v algebra/auth.v
algebra/fin_maps.v algebra/fin_maps.v
algebra/cofe.v algebra/cofe.v
algebra/base.v algebra/base.v
algebra/dra.v algebra/dra.v
algebra/cofe_solver.v algebra/cofe_solver.v
algebra/agree.v algebra/agree.v
algebra/excl.v algebra/excl.v
program_logic/model.v program_logic/model.v
program_logic/adequacy.v program_logic/adequacy.v
program_logic/hoare_lifting.v program_logic/hoare_lifting.v
(** This file is essentially a bunch of testcases. *) (** This file is essentially a bunch of testcases. *)
Require Import logic.upred. Require Import program_logic.upred.
Require Import heap_lang.lifting heap_lang.sugar. Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang. Import heap_lang.
Import uPred. Import uPred.
Require Export logic.upred program_logic.resources. Require Export program_logic.upred program_logic.resources.
Require Import algebra.cofe_solver. Require Import algebra.cofe_solver.
Module iProp. Module iProp.
Supports Markdown
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