aboutsummaryrefslogtreecommitdiffstats
path: root/src/verilog/AssocMap.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/verilog/AssocMap.v')
-rw-r--r--src/verilog/AssocMap.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v
index 5d531d5..c5cfa3f 100644
--- a/src/verilog/AssocMap.v
+++ b/src/verilog/AssocMap.v
@@ -16,7 +16,7 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*)
-From coqup Require Import Coquplib Value.
+From coqup Require Import Coquplib ValueInt.
From compcert Require Import Maps.
Definition reg := positive.
@@ -192,7 +192,7 @@ Import AssocMapExt.
Definition assocmap := AssocMap.t value.
Definition find_assocmap (n : nat) : reg -> assocmap -> value :=
- get_default value (ZToValue n 0).
+ get_default value (ZToValue 0).
Definition empty_assocmap : assocmap := AssocMap.empty value.