From e06577fe952a3c268520b280b020bb2bff252529 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 29 May 2020 18:14:59 +0100 Subject: Fix compilation moving to PTree --- src/verilog/HTL.v | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) (limited to 'src/verilog/HTL.v') 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 { -- cgit