diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 13:04:33 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-02 13:04:33 +0100 |
| commit | 707b8ef8e12ed033655161271512f962dd8906d4 (patch) | |
| tree | ad46cc5f425ae54fe07a6e5e935232ca5fcd111a /kvx/Op.v | |
| parent | 8b03b197c24e32974be1ca254039bc728d48d615 (diff) | |
| download | compcert-kvx-707b8ef8e12ed033655161271512f962dd8906d4.tar.gz compcert-kvx-707b8ef8e12ed033655161271512f962dd8906d4.zip | |
simpl -> cbn
Diffstat (limited to 'kvx/Op.v')
| -rw-r--r-- | kvx/Op.v | 18 |
1 files changed, 9 insertions, 9 deletions
@@ -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. |