1 files changed, 9 insertions, 9 deletions
diff --git a/kvx/Op.v b/kvx/Op.v
index 8856b795..4458adb3 100644
--- a/kvx/Op.v
+++ b/kvx/Op.v
@@ -1266,18 +1266,18 @@ Lemma op_valid_pointer_eq:
   (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) ->
   eval_operation ge sp op args m1 = eval_operation ge sp op args m2.
 Proof.
-  intros until m2. destruct op; simpl; try congruence.
-  - intros MEM; destruct cond; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  intros until m2. destruct op; cbn; try congruence.
+  - intros MEM; destruct cond; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
-  - intros MEM; destruct c0; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  - intros MEM; destruct c0; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
-  - intros MEM; destruct c0; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  - intros MEM; destruct c0; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
-  - intros MEM; destruct c0; simpl; try congruence;
-    repeat (destruct args; simpl; try congruence);
+  - intros MEM; destruct c0; cbn; try congruence;
+    repeat (destruct args; cbn; try congruence);
     erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto.
 Qed.