diff options
Diffstat (limited to 'riscV/SelectOpproof.v')
| -rw-r--r-- | riscV/SelectOpproof.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v index 436cd4f3..1d13702a 100644 --- a/riscV/SelectOpproof.v +++ b/riscV/SelectOpproof.v @@ -788,6 +788,7 @@ Theorem eval_intoffloat: exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold intoffloat. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_intuoffloat: @@ -797,6 +798,7 @@ Theorem eval_intuoffloat: exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. Proof. intros; unfold intuoffloat. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_floatofintu: @@ -808,6 +810,7 @@ Proof. intros until y; unfold floatofintu. case (floatofintu_match a); intros. InvEval. simpl in H0. TrivialExists. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_floatofint: @@ -819,6 +822,7 @@ Proof. intros until y; unfold floatofint. case (floatofint_match a); intros. InvEval. simpl in H0. TrivialExists. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_intofsingle: @@ -828,6 +832,7 @@ Theorem eval_intofsingle: exists v, eval_expr ge sp e m le (intofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold intofsingle. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleofint: @@ -837,6 +842,7 @@ Theorem eval_singleofint: exists v, eval_expr ge sp e m le (singleofint a) v /\ Val.lessdef y v. Proof. intros; unfold singleofint; TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_intuofsingle: @@ -846,6 +852,7 @@ Theorem eval_intuofsingle: exists v, eval_expr ge sp e m le (intuofsingle a) v /\ Val.lessdef y v. Proof. intros; unfold intuofsingle. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleofintu: @@ -855,6 +862,7 @@ Theorem eval_singleofintu: exists v, eval_expr ge sp e m le (singleofintu a) v /\ Val.lessdef y v. Proof. intros; unfold intuofsingle. TrivialExists. + cbn. rewrite H0. reflexivity. Qed. Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. |