vericert.hls.RTLBlockgen

Parameter partition : RTL.function -> Errors.res function.

Definition transl_fundef := transf_partial_fundef partition.

Definition transl_program : RTL.program -> Errors.res program :=
  transform_partial_program transl_fundef.