diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 18:14:59 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-05-29 18:14:59 +0100 |
commit | e06577fe952a3c268520b280b020bb2bff252529 (patch) | |
tree | 6a96dd75f90a81ea80108c909a98bc78ecdabd66 /src/verilog/HTL.v | |
parent | 3f3623f533033aca29fc7c5a05d2dad716133811 (diff) | |
download | vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.tar.gz vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.zip |
Fix compilation moving to PTree
Diffstat (limited to 'src/verilog/HTL.v')
-rw-r--r-- | src/verilog/HTL.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 36e4434..a21064c 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -20,6 +20,7 @@ From Coq Require Import FSets.FMapPositive. From coqup Require Import Coquplib Value AssocMap. From coqup Require Verilog. From compcert Require Events Globalenvs Smallstep Integers. +From compcert Require Import Maps. Import HexNotationValue. @@ -29,13 +30,11 @@ hardware-like layout that is still similar to the register transfer language instantiations and that we now describe a state machine instead of a control-flow graph. *) -Notation "a ! b" := (PositiveMap.find b a) (at level 1). - Definition reg := positive. Definition node := positive. -Definition datapath := PositiveMap.t Verilog.stmnt. -Definition controllogic := PositiveMap.t Verilog.stmnt. +Definition datapath := PTree.t Verilog.stmnt. +Definition controllogic := PTree.t Verilog.stmnt. Record module: Type := mkmodule { |