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/translation/HTLgenspec.v | |
| parent | 3f3623f533033aca29fc7c5a05d2dad716133811 (diff) | |
| download | vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.tar.gz vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.zip | |
Fix compilation moving to PTree
Diffstat (limited to 'src/translation/HTLgenspec.v')
| -rw-r--r-- | src/translation/HTLgenspec.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 <https://www.gnu.org/licenses/>. *) -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, |