From a7996f117769c65662b6b52d0e8f435cfc5c63dc Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 Feb 2016 14:33:50 +0100
Subject: [PATCH] Make names in hoare_lifting more consistent with those in
 lifting.

Still, there are some other inconsistencies between these two files
that may need fixing, like whether to take fork into account or not
and order of arguments.
---
 iris/hoare_lifting.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/iris/hoare_lifting.v b/iris/hoare_lifting.v
index 7bfd02e27..471502d81 100644
--- a/iris/hoare_lifting.v
+++ b/iris/hoare_lifting.v
@@ -44,7 +44,8 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
-Lemma ht_lift_atomic E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
+Lemma ht_lift_atomic_step
+    E (φ : expr Λ → state Λ → option (expr Λ) → Prop) P e1 σ1 :
   atomic e1 →
   reducible e1 σ1 →
   (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) →
@@ -94,8 +95,8 @@ Proof.
   rewrite {1}/ht -always_wand_impl always_elim wand_elim_r; apply wp_mono=>v.
   by apply const_intro.
 Qed.
-Lemma ht_lift_pure_determistic_step E
-    (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 e2 ef :
+Lemma ht_lift_pure_det_step
+    E (φ : expr Λ → option (expr Λ) → Prop) P P' Q e1 e2 ef :
   to_val e1 = None →
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef' → σ1 = σ2 ∧ e2 = e2' ∧ ef = ef')→
-- 
GitLab