From fa7415be2fe9b240374f0a51c1cd4a9de5376c5a Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 6 Sep 2006 20:00:02 +0000 Subject: Permettre les casts entre types de fonction git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@83 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cshmgenproof2.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'cfrontend/Cshmgenproof2.v') 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: -- cgit