diff options
Diffstat (limited to 'backend/Conventions.v')
| -rw-r--r-- | backend/Conventions.v | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/backend/Conventions.v b/backend/Conventions.v index 989bfa05..6025c6b4 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -128,8 +128,6 @@ Definition callee_save_loc (l: loc) := | S sl ofs ty => sl <> Outgoing end. -Hint Unfold callee_save_loc. - Definition agree_callee_save (ls1 ls2: Locmap.t) : Prop := forall l, callee_save_loc l -> ls1 l = ls2 l. |