diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 12:12:30 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-04-30 12:12:30 +0100 |
| commit | c4653db6279185a338e8b0d59a02fb7ff7ccc554 (patch) | |
| tree | 884e24f7c539a70e254f0b93dcc499af5d53bf3a /src/hls/HTLgen.v | |
| parent | 4116d7ea68e013088b3c9f7562f1a004454330aa (diff) | |
| download | vericert-c4653db6279185a338e8b0d59a02fb7ff7ccc554.tar.gz vericert-c4653db6279185a338e8b0d59a02fb7ff7ccc554.zip | |
Delete unused get_main_clk function from HTLgen
Diffstat (limited to 'src/hls/HTLgen.v')
| -rw-r--r-- | src/hls/HTLgen.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/src/hls/HTLgen.v b/src/hls/HTLgen.v index c443ae0..aa1064b 100644 --- a/src/hls/HTLgen.v +++ b/src/hls/HTLgen.v @@ -858,17 +858,6 @@ Section RENUMBER. End TRANSF_PROGRAM_STATEFUL. - Definition get_main_clk (p : HTL.program) : Errors.res reg := - let ge := Globalenvs.Genv.globalenv p in - match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with - | Some b => - match Globalenvs.Genv.find_funct_ptr ge b with - | Some (AST.Internal m) => Errors.OK (HTL.mod_clk m) - | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering") - end - | _ => Errors.Error (Errors.msg "Cannot find internal main for renumbering") - end. - Definition renumber_program (p : HTL.program) : Errors.res HTL.program := transform_stateful_program _ _ _ (fun _ f => renumber_fundef f) |