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).

5 files changed, 7 insertions, 7 deletions

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 0e3b7c8e..c08ab08b 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -305,7 +305,7 @@ Local Opaque mreg_type.
 - (* getstack *)
   simpl in *; InvBooleans.
   econstructor; eauto.
-  eapply wt_setreg; eauto. eapply Val.has_subtype; eauto. apply WTRS.
+  eapply wt_setreg; eauto. eapply Val.has_subtype; [eauto|apply WTRS].
   apply wt_undef_regs; auto.
 - (* setstack *)
   simpl in *; InvBooleans.
@@ -316,7 +316,7 @@ Local Opaque mreg_type.
   + (* move *)
     InvBooleans. exploit is_move_operation_correct; eauto. intros [EQ1 EQ2]; subst.
     simpl in H. inv H.
-    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; eauto. apply WTRS.
+    econstructor; eauto. apply wt_setreg. eapply Val.has_subtype; [eauto|apply WTRS].
     apply wt_undef_regs; auto.
   + (* other ops *)
     destruct (type_of_operation op) as [ty_args ty_res] eqn:TYOP. InvBooleans.
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. 
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).
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index ebf2c5ea..61a37180 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -339,7 +339,7 @@ Qed.
 Lemma aregs_sound:
   forall bc e ae rl, ematch bc e ae -> list_forall2 (vmatch bc) (e##rl) (aregs ae rl).
 Proof.
-  induction rl; simpl; intros. constructor. constructor; auto. apply areg_sound; auto.
+  induction rl; simpl; intros. constructor. constructor; [apply areg_sound|]; auto.
 Qed.
 
 Global Hint Resolve areg_sound aregs_sound: va.
diff --git a/lib/Integers.v b/lib/Integers.v
index 10faeefa..b69e9842 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -1263,7 +1263,7 @@ Qed.
 
 Theorem and_zero: forall x, and x zero = zero.
 Proof.
-  bit_solve. apply andb_b_false.
+  bit_solve; apply andb_b_false.
 Qed.
 
 Corollary and_zero_l: forall x, and zero x = zero.
@@ -1273,7 +1273,7 @@ Qed.
 
 Theorem and_mone: forall x, and x mone = x.
 Proof.
-  bit_solve. apply andb_b_true.
+  bit_solve; apply andb_b_true.
 Qed.
 
 Corollary and_mone_l: forall x, and mone x = x.