diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2020-01-09 15:38:45 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2020-01-09 15:38:45 +0100 |
| commit | 27767971a256b97ee75deab19a01d575ee01a6e0 (patch) | |
| tree | e0c071d856c632a5cddaeb520df09f284e5380b7 /mppa_k1c/Asmblockdeps.v | |
| parent | dc7ba7bf86828da813e60d60dc9627cbd6ddcf0e (diff) | |
| download | compcert-kvx-27767971a256b97ee75deab19a01d575ee01a6e0.tar.gz compcert-kvx-27767971a256b97ee75deab19a01d575ee01a6e0.zip | |
Fixing issue with "destruct ... in ..." tactics with Coq 8.8
Diffstat (limited to 'mppa_k1c/Asmblockdeps.v')
| -rw-r--r-- | mppa_k1c/Asmblockdeps.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 2cdf9499..584f2339 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -257,13 +257,13 @@ Proof. unfold Mem.storev in *. unfold Val.offset_ptr in *. destruct base as [ | | | | | wblock wpofs] in * ; try congruence. - destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence. + destruct (Mem.store _ _ _ _ _) eqn:E0; try congruence. inv STORE0. - destruct (Mem.store _ _ _ _) eqn:E1 in STORE1; try congruence. + destruct (Mem.store (store_chunk n2) _ _ _ _) eqn:E1; try congruence. inv STORE1. - destruct (Mem.store _ _ _ _) eqn:E0' in STORE0'; try congruence. + destruct (Mem.store (store_chunk n2) m0 _ _ _) eqn:E0'; try congruence. inv STORE0'. - destruct (Mem.store _ _ _ _) eqn:E1' in STORE1'; try congruence. + destruct (Mem.store _ m1' _ _ _) eqn:E1'; try congruence. inv STORE1'. assert (Some m2 = Some m2'). 2: congruence. @@ -310,7 +310,7 @@ Proof. unfold eval_offset in *. unfold Val.offset_ptr in *. destruct base as [ | | | | | wblock wpofs] in * ; try congruence. - destruct (Mem.store _ _ _ _) eqn:E0 in STORE0; try congruence. + destruct (Mem.store _ _ _ _) eqn:E0; try congruence. inv STORE0. assert ( (Mem.load (load_chunk n2) m1 wblock |