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/SimplExpr.v | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'cfrontend/SimplExpr.v') diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v index 089797f2..36fe07ae 100644 --- a/cfrontend/SimplExpr.v +++ b/cfrontend/SimplExpr.v @@ -540,5 +540,10 @@ Fixpoint transl_globdefs end. Definition transl_program (p: Csyntax.program) : res program := - do gl' <- transl_globdefs p.(prog_defs) (initial_generator tt); - OK (mkprogram gl' p.(prog_public) p.(prog_main)). + do gl' <- transl_globdefs (Csyntax.prog_defs p) (initial_generator tt); + OK {| prog_defs := gl'; + prog_public := Csyntax.prog_public p; + prog_main := Csyntax.prog_main p; + prog_types := Csyntax.prog_types p; + prog_comp_env := Csyntax.prog_comp_env p; + prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}. -- cgit