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/AssocMap.v | |
| parent | 3f3623f533033aca29fc7c5a05d2dad716133811 (diff) | |
| download | vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.tar.gz vericert-kvx-e06577fe952a3c268520b280b020bb2bff252529.zip | |
Fix compilation moving to PTree
Diffstat (limited to 'src/verilog/AssocMap.v')
| -rw-r--r-- | src/verilog/AssocMap.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/verilog/AssocMap.v b/src/verilog/AssocMap.v index 43f9065..88b13a6 100644 --- a/src/verilog/AssocMap.v +++ b/src/verilog/AssocMap.v @@ -198,6 +198,10 @@ Definition empty_assocmap : assocmap := AssocMap.empty value. Definition merge_assocmap : assocmap -> assocmap -> assocmap := merge value. +Ltac unfold_merge := + unfold merge_assocmap; try (repeat (rewrite merge_add_assoc)); + rewrite AssocMapExt.merge_base_1. + Module AssocMapNotation. Notation "a ! b" := (AssocMap.get b a) (at level 1). Notation "a # ( b , c )" := (find_assocmap c b a) (at level 1). |