From cb27aa7f3512c87fbc712c42e356de51634cdac9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 1 Jul 2019 11:07:15 +0200
Subject: [PATCH] use decide instead of bool_decide where possible
---
theories/heap_lang/lang.v | 2 +-
theories/heap_lang/lifting.v | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 1d6861cdb..7ab1f4c18 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -520,7 +520,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
Definition bin_op_eval (op : bin_op) (v1 v2 : val) : option val :=
if decide (op = EqOp) then
(* Crucially, this compares the same way as [CmpXchg]! *)
- if bool_decide (vals_compare_safe v1 v2) then
+ if decide (vals_compare_safe v1 v2) then
Some $ LitV $ LitBool $ bool_decide (v1 = v2)
else
None
diff --git a/theories/heap_lang/lifting.v b/theories/heap_lang/lifting.v
index 8dda1c8f2..48b9cbe70 100644
--- a/theories/heap_lang/lifting.v
+++ b/theories/heap_lang/lifting.v
@@ -172,7 +172,7 @@ Proof.
intros Hcompare.
cut (bin_op_eval EqOp v1 v2 = Some $ LitV $ LitBool $ bool_decide (v1 = v2)).
{ intros. revert Hcompare. solve_pure_exec. }
- rewrite /bin_op_eval /= bool_decide_true //.
+ rewrite /bin_op_eval /= decide_True //.
Qed.
Instance pure_if_true e1 e2 : PureExec True 1 (If (Val $ LitV $ LitBool true) e1 e2) e1.
--
GitLab