From d741845da605f75a3cf650fe2915940ce58ddaa5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 6 May 2015 11:26:27 +0200 Subject: Typo: Val.sun_inject -> Val.sub_inject. --- arm/Op.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'arm/Op.v') diff --git a/arm/Op.v b/arm/Op.v index b5ea9a7a..df39b26a 100644 --- a/arm/Op.v +++ b/arm/Op.v @@ -878,10 +878,10 @@ Proof. apply Values.Val.add_inject; auto. apply eval_shift_inj; auto. apply Values.Val.add_inject; auto. - apply Values.Val.sun_inject; auto. - apply Values.Val.sun_inject; auto. apply eval_shift_inj; auto. - apply Values.Val.sun_inject; auto. apply eval_shift_inj; auto. - apply (@Values.Val.sun_inject f (Vint i) (Vint i) v v'); auto. + apply Values.Val.sub_inject; auto. + apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. + apply Values.Val.sub_inject; auto. apply eval_shift_inj; auto. + apply (@Values.Val.sub_inject f (Vint i) (Vint i) v v'); auto. inv H4; inv H2; simpl; auto. apply Values.Val.add_inject; auto. inv H4; inv H2; simpl; auto. -- cgit