From 56ea621762c865c1c71bdc7ad99afc4f2c291d5c Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sat, 7 Nov 2020 10:13:22 +0000
Subject: Update definition of Vneg

---
 src/common/IntegerExtra.v | 2 +-
 src/hls/Verilog.v         | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index 8b11823..f44cac2 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -639,7 +639,7 @@ Module IntExtra.
     apply unsigned_range_2.
   Qed.
 
-  Lemma shrx_shrx_alt_equiv :
+  Theorem shrx_shrx_alt_equiv :
     forall x y,
       unsigned y <= 30 ->
       shrx x y = shrx_alt x y.
diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index c5dab9e..e5f86d5 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -149,7 +149,7 @@ Inductive binop : Type :=
 (** ** Unary Operators *)
 
 Inductive unop : Type :=
-| Vneg  (** negation ([~]) *)
+| Vneg  (** negation ([-]) *)
 | Vnot. (** not operation [!] *)
 
 (** ** Expressions *)
-- 
cgit