Rename program_logic/ectx_weakestpre.v → program_logic/ectx_lifting.v.

e54910b7 · Robbert Krebbers · 497cb7fa · e54910b7 · e54910b7 · e54910b7
Commit e54910b7 authored May 09, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 3 deletions

_CoqProject _CoqProject +1 -1

heap_lang/lifting.v heap_lang/lifting.v +2 -2

program_logic/ectx_lifting.v program_logic/ectx_lifting.v +0 -0

No files found.
--- a/_CoqProject
+++ b/_CoqProject
@@ -73,7 +73,7 @@ program_logic/hoare.v
 program_logic/language.v
 program_logic/ectx_language.v
 program_logic/ectxi_language.v
-program_logic/ectx_weakestpre.v
+program_logic/ectx_lifting.v
 program_logic/ghost_ownership.v
 program_logic/global_functor.v
 program_logic/saved_prop.v

--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
-From iris.program_logic Require Export ectx_weakestpre.
-From iris.program_logic Require Import ownership. (* for ownP *)
+From iris.program_logic Require Export weakestpre.
+From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *)
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import weakestpre.

--- a/program_logic/ectx_weakestpre.v
+++ b/program_logic/ectx_weakestpre.v