diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-30 14:42:28 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-30 14:42:28 +0200 |
| commit | 244159573aa20a0a74897edb5897ded1bd16cd66 (patch) | |
| tree | f6c622076e43794b143dbab8da6f9c526900215a /aarch64/SelectOpproof.v | |
| parent | 154529f64b96ca0e4cef8c4aeff6a1cfb8210e91 (diff) | |
| download | compcert-kvx-244159573aa20a0a74897edb5897ded1bd16cd66.tar.gz compcert-kvx-244159573aa20a0a74897edb5897ded1bd16cd66.zip | |
non trapping op
Diffstat (limited to 'aarch64/SelectOpproof.v')
| -rw-r--r-- | aarch64/SelectOpproof.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/aarch64/SelectOpproof.v b/aarch64/SelectOpproof.v index c7898193..9ce7a8bf 100644 --- a/aarch64/SelectOpproof.v +++ b/aarch64/SelectOpproof.v @@ -932,7 +932,7 @@ Theorem eval_intoffloat: Val.intoffloat x = Some y -> exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v. Proof. - intros; TrivialExists. + intros; TrivialExists. cbn. rewrite H0. reflexivity. Qed. Theorem eval_floatofint: @@ -943,7 +943,7 @@ Theorem eval_floatofint: Proof. intros until y; unfold floatofint. case (floatofint_match a); intros; InvEval. - TrivialExists. -- TrivialExists. +- TrivialExists. cbn. rewrite H0. reflexivity. Qed. Theorem eval_intuoffloat: @@ -952,7 +952,7 @@ Theorem eval_intuoffloat: Val.intuoffloat x = Some y -> exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. - intros; TrivialExists. + intros; TrivialExists. cbn. rewrite H0. reflexivity. Qed. Theorem eval_floatofintu: @@ -963,7 +963,7 @@ Theorem eval_floatofintu: Proof. intros until y; unfold floatofintu. case (floatofintu_match a); intros; InvEval. - TrivialExists. -- TrivialExists. +- TrivialExists. cbn. rewrite H0. reflexivity. Qed. Theorem eval_intofsingle: @@ -972,7 +972,7 @@ Theorem eval_intofsingle: Val.intofsingle x = Some y -> exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v. Proof. - intros; TrivialExists. + intros; TrivialExists. cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleofint: @@ -983,7 +983,7 @@ Theorem eval_singleofint: Proof. intros until y; unfold singleofint. case (singleofint_match a); intros; InvEval. - TrivialExists. -- TrivialExists. +- TrivialExists. cbn. rewrite H0. reflexivity. Qed. Theorem eval_intuofsingle: @@ -992,7 +992,7 @@ Theorem eval_intuofsingle: Val.intuofsingle x = Some y -> exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v. Proof. - intros; TrivialExists. + intros; TrivialExists. cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleofintu: @@ -1003,7 +1003,7 @@ Theorem eval_singleofintu: Proof. intros until y; unfold singleofintu. case (singleofintu_match a); intros; InvEval. - TrivialExists. -- TrivialExists. +- TrivialExists. cbn. rewrite H0. reflexivity. Qed. (** Selection *) |