diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-01-23 13:33:33 +0100 |
| commit | b5b681b7b55abb18165eaa907b04aefb9b0fddde (patch) | |
| tree | 9c0a7df4b20ede85b54fe5c4e5d326fbf30a0013 /cfrontend/SimplExprspec.v | |
| parent | 12803784f2753863985d1030999469c18e01e0f1 (diff) | |
| parent | f00b70b6a17fdfb4e8606df891f6becc8102ef12 (diff) | |
| download | compcert-kvx-b5b681b7b55abb18165eaa907b04aefb9b0fddde.tar.gz compcert-kvx-b5b681b7b55abb18165eaa907b04aefb9b0fddde.zip | |
Merge branch 'master' into dwarf
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. |