aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/Verilog.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-07-03 21:05:45 +0100
committerYann Herklotz <git@yannherklotz.com>2020-07-03 21:05:45 +0100
commit594c2825012d94675317f51cf6a3e97c2f88cd02 (patch)
tree19c6b85504a9040cb48161325cdda14208ae9155 /src/verilog/Verilog.v
parentb5144a6f513c5c6e3344dcc935117706637ddd3f (diff)
downloadvericert-594c2825012d94675317f51cf6a3e97c2f88cd02.tar.gz
vericert-594c2825012d94675317f51cf6a3e97c2f88cd02.zip
Fixing HTLgenproof
Diffstat (limited to 'src/verilog/Verilog.v')
-rw-r--r--src/verilog/Verilog.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/verilog/Verilog.v b/src/verilog/Verilog.v
index 5ef4dda..f5916ad 100644
--- a/src/verilog/Verilog.v
+++ b/src/verilog/Verilog.v
@@ -331,7 +331,7 @@ Definition binop_run (op : binop) (v1 v2 : value) : option value :=
Definition unop_run (op : unop) (v1 : value) : value :=
match op with
- | Vneg => Int.notbool v1
+ | Vneg => Int.neg v1
| Vnot => Int.not v1
end.