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 6f6afa8a..0b7643c6 100644 --- a/arm/ConstpropOpproof.v +++ b/arm/ConstpropOpproof.v @@ -98,7 +98,7 @@ Ltac SimplVM := Lemma eval_static_shift_correct: forall s n, eval_shift s (Vint n) = Vint (eval_static_shift s n). Proof. - intros. destruct s; simpl; rewrite s_range; auto. + intros. destruct s; simpl; rewrite ? s_range; auto. Qed. Lemma cond_strength_reduction_correct: |