diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-18 22:49:10 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-10-18 22:49:10 +0200 |
| commit | 996a2e5bbc4826d95144b62f5218b6e3e1e7d881 (patch) | |
| tree | 55a5136c68e7d0f7a304913f28d0a761d9facd9a /kvx/SelectOpproof.v | |
| parent | 8c3a2bdb56eba8d8bc5e359b01a320916eac85f0 (diff) | |
| parent | a2f31f2b886ccb9656a019db1780aabc1789368a (diff) | |
| download | compcert-kvx-996a2e5bbc4826d95144b62f5218b6e3e1e7d881.tar.gz compcert-kvx-996a2e5bbc4826d95144b62f5218b6e3e1e7d881.zip | |
Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass
Diffstat (limited to 'kvx/SelectOpproof.v')
| -rw-r--r-- | kvx/SelectOpproof.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/kvx/SelectOpproof.v b/kvx/SelectOpproof.v index c23ed601..7a301929 100644 --- a/kvx/SelectOpproof.v +++ b/kvx/SelectOpproof.v @@ -1547,6 +1547,15 @@ Proof. intros until b. intro Hop; injection Hop; clear Hop; intro; subst a. intros HeL He1 He2 HeC. + destruct same_expr_pure eqn:SAME. + { + destruct (eval_same_expr a1 a2 le v1 v2 SAME He1 He2) as [EQ1 EQ2]. + subst a2. subst v2. + exists v1; split; trivial. + cbn. + rewrite if_same. + apply Val.lessdef_normalize. + } unfold cond_to_condition0. destruct (cond_to_condition0_match cond al). { |