From e89f1e606bc8c9c425628392adc9c69cec666b5e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 22 Dec 2014 19:34:45 +0100 Subject: Represent struct and union types by name instead of by structure. --- cfrontend/SimplExprspec.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'cfrontend/SimplExprspec.v') diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v index 83ddd1f4..9f9fb450 100644 --- a/cfrontend/SimplExprspec.v +++ b/cfrontend/SimplExprspec.v @@ -1144,10 +1144,10 @@ Qed. Theorem transl_program_spec: forall p tp, transl_program p = OK tp -> - match_program tr_fundef (fun v1 v2 => v1 = v2) nil p.(prog_main) p tp. + match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp. Proof. unfold transl_program; intros. - destruct (transl_globdefs (prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H. + destruct (transl_globdefs (Csyntax.prog_defs p) (initial_generator tt)) eqn:E; simpl in H; inv H. split; auto. exists l; split. eapply transl_globdefs_spec; eauto. rewrite <- app_nil_end; auto. Qed. -- cgit