From 6df33dacfcd3c0b6d7729707e31a99867a8e2c06 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 4 Oct 2017 11:27:42 +0900
Subject: [PATCH] More consistent naming for `pure_exec`.

---
 theories/heap_lang/lifting.v           | 22 +++++++++++-----------
 theories/program_logic/ectx_language.v |  2 +-
 theories/program_logic/language.v      |  2 +-
 3 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 6d6e5762e..b8d1570db 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -82,49 +82,49 @@ Qed.
 
 Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
 Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
-Local Ltac solve_pureexec :=
+Local Ltac solve_pure_exec :=
   repeat lazymatch goal with
   | H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H
   | H: AsRec _ _ _ _ |- _ => rewrite H; clear H
   end;
-  apply det_head_step_pureexec; [ solve_exec_safe | solve_exec_puredet ].
+  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
 
 Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val)
     `{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
   PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_unop op e v v' `{!IntoVal e v} :
   PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
   PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_if_true e1 e2 :
   PureExec True (If (Lit (LitBool true)) e1 e2) e1.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_if_false e1 e2 :
   PureExec True (If (Lit (LitBool false)) e1 e2) e2.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
   PureExec True (Fst (Pair e1 e2)) e1.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} :
   PureExec True (Snd (Pair e1 e2)) e2.
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 Global Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
   PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
-Proof. solve_pureexec. Qed.
+Proof. solve_pure_exec. Qed.
 
 (** Heap *)
 Lemma wp_alloc E e v :
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 78bc50820..65da78ed1 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -151,7 +151,7 @@ Section ectx_language.
       econstructor; eauto.
   Qed.
 
-  Lemma det_head_step_pureexec (P : Prop) e1 e2 :
+  Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
     (∀ σ, P → head_reducible e1 σ) →
     (∀ σ1 e2' σ2 efs,
       P → head_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2=e2' ∧ efs = []) →
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index b884a3085..88c82f8eb 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -101,7 +101,7 @@ Section language.
       P → prim_step e1 σ1 e2' σ2 efs → σ1 = σ2 ∧ e2 = e2' ∧ efs = [];
   }.
 
-  Lemma hoist_pred_pureexec (P : Prop) (e1 e2 : expr Λ) :
+  Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
     (P → PureExec True e1 e2) →
     PureExec P e1 e2.
   Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
-- 
GitLab