diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-22 19:34:45 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2014-12-22 19:34:45 +0100 |
| commit | e89f1e606bc8c9c425628392adc9c69cec666b5e (patch) | |
| tree | 9c1d9bccb0811666a5f51c89a4285a4d747f34b7 /cfrontend/SimplExprspec.v | |
| parent | f1db887befa816f70f64aaffa2ce4d92c4bebc55 (diff) | |
| download | compcert-kvx-e89f1e606bc8c9c425628392adc9c69cec666b5e.tar.gz compcert-kvx-e89f1e606bc8c9c425628392adc9c69cec666b5e.zip | |
Represent struct and union types by name instead of by structure.
Diffstat (limited to 'cfrontend/SimplExprspec.v')
| -rw-r--r-- | cfrontend/SimplExprspec.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |