diff options
Diffstat (limited to 'backend/Unusedglob.v')
| -rw-r--r-- | backend/Unusedglob.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v index 916e111b..8ac7c4ce 100644 --- a/backend/Unusedglob.v +++ b/backend/Unusedglob.v @@ -107,7 +107,7 @@ Definition used_globals (p: program) (pm: prog_map) : option IS.t := (** * Elimination of unreferenced global definitions *) -(** We also eliminate multiple definitions of the same global name, keeping ony +(** We also eliminate multiple definitions of the same global name, keeping only the last definition (in program definition order). *) Fixpoint filter_globdefs (used: IS.t) (accu defs: list (ident * globdef fundef unit)) := |