diff options
Diffstat (limited to 'backend/RTL.v')
| -rw-r--r-- | backend/RTL.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTL.v b/backend/RTL.v index 1c309a0..208c7b1 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -368,7 +368,7 @@ Definition successors_instr (i: instruction) : list node := end. Definition successors (f: function) : PTree.t (list node) := - PTree.map (fun pc i => successors_instr i) f.(fn_code). + PTree.map1 successors_instr f.(fn_code). (** Transformation of a RTL function instruction by instruction. This applies a given transformation function to all instructions |