aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/ValueInt.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/ValueInt.v')
-rw-r--r--src/verilog/ValueInt.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index 2220998..f1fd056 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -77,7 +77,6 @@ Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i.
Definition valueToPtr (i : value) : Integers.ptrofs :=
Ptrofs.of_int i.
-Search Ptrofs.of_int Ptrofs.to_int.
Definition valToValue (v : Values.val) : option value :=
match v with
| Values.Vint i => Some (intToValue i)