From e54910b73e26b4a8f64b7699088e7ecaa2012b73 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 May 2016 10:40:19 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20program=5Flogic/ectx=5Fweakestpre.v=20?=
=?UTF-8?q?=E2=86=92=20program=5Flogic/ectx=5Flifting.v.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
_CoqProject | 2 +-
heap_lang/lifting.v | 4 ++--
program_logic/{ectx_weakestpre.v => ectx_lifting.v} | 0
3 files changed, 3 insertions(+), 3 deletions(-)
rename program_logic/{ectx_weakestpre.v => ectx_lifting.v} (100%)
diff --git a/_CoqProject b/_CoqProject
index 570535e83..46417a253 100644
--- 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
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 157125e22..91b78c4f1 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,5 +1,5 @@
-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.
diff --git a/program_logic/ectx_weakestpre.v b/program_logic/ectx_lifting.v
similarity index 100%
rename from program_logic/ectx_weakestpre.v
rename to program_logic/ectx_lifting.v
--
GitLab