aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/common/IntegerExtra.v2
-rw-r--r--src/hls/Verilog.v2
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 *)