diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-02-27 18:02:33 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-02-27 18:02:33 +0100 |
| commit | f50d5b2e7d689a0033943fca270d322b33c1a781 (patch) | |
| tree | d6c5747ed7ff2ae2ceb0f2ae430b43ab576f351c /mppa_k1c/SelectLongproof.v | |
| parent | b09dea1ebfa5358e4d866e03e5a024c968c6a0b8 (diff) | |
| download | compcert-kvx-f50d5b2e7d689a0033943fca270d322b33c1a781.tar.gz compcert-kvx-f50d5b2e7d689a0033943fca270d322b33c1a781.zip | |
Float conversion fixes + some more conversions
Diffstat (limited to 'mppa_k1c/SelectLongproof.v')
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v index d12fb9ae..44846a6f 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -582,30 +582,30 @@ Qed. Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. Proof. - unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL. + unfold longofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_longofsingle; eauto. - TrivialExists. +(* TrivialExists. *) Qed. Theorem eval_longuofsingle: partial_unary_constructor_sound longuofsingle Val.longuofsingle. Proof. - unfold longuofsingle; red; intros. destruct Archi.splitlong eqn:SL. + unfold longuofsingle; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_longuofsingle; eauto. - TrivialExists. +(* TrivialExists. *) Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. Proof. - unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL. + unfold singleoflong; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_singleoflong; eauto. - TrivialExists. +(* TrivialExists. *) Qed. Theorem eval_singleoflongu: partial_unary_constructor_sound singleoflongu Val.singleoflongu. Proof. - unfold singleoflongu; red; intros. destruct Archi.splitlong eqn:SL. + unfold singleoflongu; red; intros. (* destruct Archi.splitlong eqn:SL. *) eapply SplitLongproof.eval_singleoflongu; eauto. - TrivialExists. +(* TrivialExists. *) Qed. End CMCONSTR. |