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/translation/HTLgenspec.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/translation/HTLgenspec.v') diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v index b9d483c..5a61a9c 100644 --- a/src/translation/HTLgenspec.v +++ b/src/translation/HTLgenspec.v @@ -16,8 +16,8 @@ * along with this program. If not, see . *) -From Coq Require Import FSets.FMapPositive. From compcert Require RTL Op Maps Errors. +From compcert Require Import Maps. From coqup Require Import Coquplib Verilog Value HTL HTLgen AssocMap. Hint Resolve Maps.PTree.elements_keys_norepet : htlspec. @@ -160,7 +160,7 @@ Inductive tr_instr (fin rtrn st : reg) : RTL.instruction -> stmnt -> stmnt -> Pr (Vseq (block fin (Vlit (ZToValue 1%nat 1%Z))) (block rtrn (Vvar r))) Vskip. Hint Constructors tr_instr : htlspec. -Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PositiveMap.t stmnt) +Inductive tr_code (pc : RTL.node) (i : RTL.instruction) (stmnts trans : PTree.t stmnt) (fin rtrn st : reg) : Prop := tr_code_intro : forall s t, -- cgit