diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:10:22 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 12:10:22 +0100 |
commit | f6569b736d4ded08a011f55bd6001c89e899fd5c (patch) | |
tree | cc76bb6b36dc7cfc2fc5fc2b216c5b1cde0ab752 /src/hls/ClockRegisters.v | |
parent | 86e64fd05cea7b1da996701cd3653db5f471f8d1 (diff) | |
download | vericert-f6569b736d4ded08a011f55bd6001c89e899fd5c.tar.gz vericert-f6569b736d4ded08a011f55bd6001c89e899fd5c.zip |
Add comments next to admitted theorems
Diffstat (limited to 'src/hls/ClockRegisters.v')
-rw-r--r-- | src/hls/ClockRegisters.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/hls/ClockRegisters.v b/src/hls/ClockRegisters.v index 4b1c37a..fee89fb 100644 --- a/src/hls/ClockRegisters.v +++ b/src/hls/ClockRegisters.v @@ -234,7 +234,7 @@ Program Definition transf_module (m: DHTL.module) : option DHTL.module := | _ => None end. Next Obligation. -Admitted. +Admitted. (* This translation pass is only used for testing. *) Definition transl_module (m : DHTL.module) : Errors.res DHTL.module := Verilog.handle_opt (Errors.msg "ClockRegisters: not translated") (transf_module m). |