diff options
Diffstat (limited to 'arm/ConstpropOpproof.v')
| -rw-r--r-- | arm/ConstpropOpproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v index e1ae80a2..c9f97aa8 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -116,7 +116,7 @@ Proof. + (* global *) inv H2. exists (Genv.symbol_address ge id ofs); auto. + (* stack *) - inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. + inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_static_shift_correct: |