diff options
Diffstat (limited to 'backend/Selection.v')
| -rw-r--r-- | backend/Selection.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index abda1d95..f278ed0b 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -339,7 +339,7 @@ Definition sel_fundef (dm: PTree.t globdef) (hf: helper_functions) (f: Cminor.fu (** We build a partial mapping from global identifiers to their definitions, restricting ourselves to the globals we are interested in, namely the external function declarations that are marked as runtime library - helpers. + helpers. This ensures that the mapping remains small and that [lookup_helper] below is efficient. *) @@ -350,7 +350,7 @@ Definition globdef_of_interest (gd: globdef) : bool := end. Definition record_globdefs (defmap: PTree.t globdef) : PTree.t globdef := - PTree.fold + PTree.fold (fun m id gd => if globdef_of_interest gd then PTree.set id gd m else m) defmap (PTree.empty globdef). |