diff options
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 328f724..898c4df 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -517,10 +517,14 @@ Proof. exists (ev1 :: eargs''); split. simpl; constructor; auto. simpl. congruence. } - destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto; - exists eargs''; split; auto; simpl; f_equal; auto; - generalize (MATCH arg); rewrite E2; simpl; intros E3; - rewrite E3 in H5; inv H5; auto. + destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto. + * exists eargs''; split; auto; simpl; f_equal; auto. + generalize (MATCH arg); rewrite E2; simpl; intros E3; + rewrite E3 in H5; inv H5; auto. + * destruct (generate_float_constants tt); inv H1; auto. + exists eargs''; split; auto; simpl; f_equal; auto. + generalize (MATCH arg); rewrite E2; simpl; intros E3; + rewrite E3 in H5; inv H5; auto. + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E. inv H. exploit IHtargs; eauto. intros [eargs'' [A B]]. |