diff options
Diffstat (limited to 'mppa_k1c/Machblockgen.v')
| -rw-r--r-- | mppa_k1c/Machblockgen.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index c20889b7..1d5555df 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -563,7 +563,7 @@ Proof. Qed. (* à finir pour passer des Mach.function au function, etc. *) -Definition trans_function (f: Mach.function) : function := +Definition transf_function (f: Mach.function) : function := {| fn_sig:=Mach.fn_sig f; fn_code:=trans_code (Mach.fn_code f); fn_stacksize := Mach.fn_stacksize f; @@ -571,8 +571,8 @@ Definition trans_function (f: Mach.function) : function := fn_retaddr_ofs := Mach.fn_retaddr_ofs f |}. -Definition trans_fundef (f: Mach.fundef) : fundef := - transf_fundef trans_function f. +Definition transf_fundef (f: Mach.fundef) : fundef := + transf_fundef transf_function f. Definition transf_program (src: Mach.program) : program := - transform_program trans_fundef src. + transform_program transf_fundef src. |