From 707b8ef8e12ed033655161271512f962dd8906d4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 2 Dec 2020 13:04:33 +0100 Subject: simpl -> cbn --- kvx/Op.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'kvx/Op.v') 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. -- cgit