Commit 61840d31 authored by Ralf Jung's avatar Ralf Jung
Browse files

move gen_heap to base_logic. It does not depend on WP or antyhing language-specific.

parent 69d1bf6f
Pipeline #3476 failed with stage
in 11 minutes and 15 seconds
...@@ -83,6 +83,7 @@ theories/base_logic/lib/na_invariants.v ...@@ -83,6 +83,7 @@ theories/base_logic/lib/na_invariants.v
theories/base_logic/lib/cancelable_invariants.v theories/base_logic/lib/cancelable_invariants.v
theories/base_logic/lib/counter_examples.v theories/base_logic/lib/counter_examples.v
theories/base_logic/lib/fractional.v theories/base_logic/lib/fractional.v
theories/base_logic/lib/gen_heap.v
theories/program_logic/adequacy.v theories/program_logic/adequacy.v
theories/program_logic/lifting.v theories/program_logic/lifting.v
theories/program_logic/weakestpre.v theories/program_logic/weakestpre.v
...@@ -91,7 +92,6 @@ theories/program_logic/language.v ...@@ -91,7 +92,6 @@ theories/program_logic/language.v
theories/program_logic/ectx_language.v theories/program_logic/ectx_language.v
theories/program_logic/ectxi_language.v theories/program_logic/ectxi_language.v
theories/program_logic/ectx_lifting.v theories/program_logic/ectx_lifting.v
theories/program_logic/gen_heap.v
theories/program_logic/ownp.v theories/program_logic/ownp.v
theories/heap_lang/lang.v theories/heap_lang/lang.v
theories/heap_lang/tactics.v theories/heap_lang/tactics.v
......
From iris.program_logic Require Export weakestpre gen_heap. From iris.base_logic Require Export gen_heap.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ectx_lifting. From iris.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics. From iris.heap_lang Require Import tactics.
......
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