diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-06 20:00:02 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-09-06 20:00:02 +0000 |
| commit | fa7415be2fe9b240374f0a51c1cd4a9de5376c5a (patch) | |
| tree | 09132c3da985ed1051368743449e8f8432555529 /cfrontend/Cshmgenproof2.v | |
| parent | 708cd2c7767b497b9ac3dae1ce51973195d00acc (diff) | |
| download | compcert-fa7415be2fe9b240374f0a51c1cd4a9de5376c5a.tar.gz compcert-fa7415be2fe9b240374f0a51c1cd4a9de5376c5a.zip | |
Permettre les casts entre types de fonction
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@83 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cshmgenproof2.v')
| -rw-r--r-- | cfrontend/Cshmgenproof2.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 602e33a9..1a5eaa0a 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -373,7 +373,7 @@ Lemma make_cast_correct: Proof. unfold make_cast, make_cast1, make_cast2, make_unop. intros until v'; intros EVAL CAST. - inversion CAST; clear CAST; subst; auto. + inversion CAST; clear CAST; subst. (* cast_int_int *) destruct sz2; destruct si2; repeat econstructor; eauto with cshm. (* cast_float_int *) @@ -382,6 +382,10 @@ Proof. destruct sz2; destruct si1; unfold make_floatofint, make_unop; repeat econstructor; eauto with cshm; simpl; auto. (* cast_float_float *) destruct sz2; repeat econstructor; eauto with cshm. + (* neutral, ptr *) + inversion H0; auto; inversion H; auto. + (* neutral, int *) + inversion H0; auto; inversion H; auto. Qed. Lemma make_load_correct: |