diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-02 10:41:29 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-08-05 18:33:17 +0200 |
| commit | 6f737edae4b7e6243a9f11e74614f55381f62ec7 (patch) | |
| tree | 9f571037b7bc16a9cd770151853876ee066069dd /backend/Conventions.v | |
| parent | ff1ead9fe0d816918f13e1586ecfed321f4a3bf3 (diff) | |
| download | compcert-kvx-6f737edae4b7e6243a9f11e74614f55381f62ec7.tar.gz compcert-kvx-6f737edae4b7e6243a9f11e74614f55381f62ec7.zip | |
Coq 8.10 compatibility: make explicit the "core" hint database
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
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. |