aboutsummaryrefslogtreecommitdiffstats
path: root/backend/RTLgenproof.v
diff options
context:
space:
mode:
authorAndrej Dudenhefner <31094379+mrhaandi@users.noreply.github.com>2022-09-08 15:59:56 +0200
committerGitHub <noreply@github.com>2022-09-08 15:59:56 +0200
commit88cccb19502dfec65f7e21d0f6772ba99b1fb99d (patch)
tree368ad5555ff5459c1fdb4fa597db96664e4930f0 /backend/RTLgenproof.v
parent108d60c059949e34c07719cb3ce38b8c62d27e0d (diff)
downloadcompcert-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/RTLgenproof.v')
-rw-r--r--backend/RTLgenproof.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 1602823f..79b9319b 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1010,7 +1010,7 @@ Lemma invert_eval_builtin_arg:
/\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v
/\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')).
Proof.
- induction 1; simpl; try (econstructor; intuition eauto with evalexpr barg; fail).
+ induction 1; simpl. 2-8: try (econstructor; intuition eauto with evalexpr barg; fail).
- econstructor; split; eauto with evalexpr. split. constructor. auto.
- econstructor; split; eauto with evalexpr. split. constructor. auto.
- econstructor; split; eauto with evalexpr. split. repeat constructor. auto.