A fix for #5390 (a useful error on used introduction names was masked).

With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.

We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.

Of course, the question of what best unification error to give in the
presence of backtracking is still open.

2 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 239edd1da..19c9fc442 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -2,3 +2,7 @@ Ltac f H := split; [ a H | e H ]
 Ltac g := match goal with
           | |- context [ if ?X then _ else _ ] => case X
           end
+The command has indeed failed with message:
+H is already used.
+The command has indeed failed with message:
+H is already used.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index a7c497cfa..9a5edb813 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -11,3 +11,13 @@ Print Ltac f.
 
 Ltac g := match goal with |- context [if ?X then _ else _ ] => case X end.
 Print Ltac g.
+
+(* Test an error message (#5390) *)
+Lemma myid (P : Prop) : P <-> P.
+Proof. split; auto. Qed.
+
+Goal True -> (True /\ True) -> True.
+Proof.
+intros H.
+Fail intros [H%myid ?].
+Fail destruct 1 as [H%myid ?].