Commit 78f10027 authored by Ralf Jung's avatar Ralf Jung

rename op_rules -> lifting

parent 6b8069fa
Pipeline #3295 canceled with stage
......@@ -95,8 +95,8 @@ theories/program_logic/gen_heap.v
theories/program_logic/ownp.v
theories/heap_lang/lang.v
theories/heap_lang/tactics.v
theories/heap_lang/lifting.v
theories/heap_lang/wp_tactics.v
theories/heap_lang/op_rules.v
theories/heap_lang/notation.v
theories/heap_lang/lib/spawn.v
theories/heap_lang/lib/par.v
......
From iris.program_logic Require Export weakestpre adequacy gen_heap.
From iris.heap_lang Require Export op_rules.
From iris.heap_lang Require Export lifting.
From iris.algebra Require Import auth.
From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics.
......
......@@ -52,7 +52,7 @@ Local Hint Constructors head_step.
Local Hint Resolve alloc_fresh.
Local Hint Resolve to_of_val.
Section rules.
Section lifting.
Context `{heapG Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val iProp Σ.
......@@ -276,4 +276,4 @@ Proof.
intros. rewrite -wp_bin_op //; [].
destruct (bool_decide_reflect (v1 = v2)); by eauto.
Qed.
End rules.
End lifting.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import coq_tactics.
From iris.proofmode Require Export tactics.
From iris.heap_lang Require Export wp_tactics op_rules.
From iris.heap_lang Require Export wp_tactics lifting.
Import uPred.
Ltac wp_strip_later ::= iNext.
......
From iris.heap_lang Require Export tactics op_rules.
From iris.heap_lang Require Export tactics lifting.
Import uPred.
(** wp-specific helper 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