diff options
| author | Andrej Dudenhefner <31094379+mrhaandi@users.noreply.github.com> | 2022-09-08 15:59:56 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-09-08 15:59:56 +0200 |
| commit | 88cccb19502dfec65f7e21d0f6772ba99b1fb99d (patch) | |
| tree | 368ad5555ff5459c1fdb4fa597db96664e4930f0 /backend/Stackingproof.v | |
| parent | 108d60c059949e34c07719cb3ce38b8c62d27e0d (diff) | |
| download | compcert-88cccb19502dfec65f7e21d0f6772ba99b1fb99d.tar.gz compcert-88cccb19502dfec65f7e21d0f6772ba99b1fb99d.zip | |
Improved auto goal selection (#443)
Improves robustness in case of stronger (e)auto.
This is in preparation of a change in Coq that will make auto and eauto stronger
(https://github.com/coq/coq/pull/16293).
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 7724c5d6..eb613bad 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -939,7 +939,7 @@ Local Opaque mreg_type. apply range_contains in SEP; auto. exploit (contains_set_stack (fun v' => Val.inject j (ls (R r)) v') (rs r)). eexact SEP. - apply load_result_inject; auto. apply wt_ls. + apply load_result_inject; [auto|apply wt_ls]. clear SEP; intros (m1 & STORE & SEP). set (rs1 := undef_regs (destroyed_by_setstack ty) rs). assert (AG1: agree_regs j ls rs1). |