From 741f3fab052b91eaec57f32b639ca722c3d8dc34 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 12 Mar 2017 13:18:42 +0100
Subject: 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.
---
 COMPATIBILITY                 |  7 +++++++
 tactics/tactics.ml            | 40 ++++++++++++++++++++++++++++++++++++----
 test-suite/output/Tactics.out |  4 ++++
 test-suite/output/Tactics.v   | 10 ++++++++++
 4 files changed, 57 insertions(+), 4 deletions(-)

diff --git a/COMPATIBILITY b/COMPATIBILITY
index d423e71df3..78dfabaa3e 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -1,3 +1,10 @@
+Potential sources of incompatibilities between Coq V8.6 and V8.7
+----------------------------------------------------------------
+
+- Extra superfluous names in introduction patterns may now raise an
+  error rather than a warning when the superfluous name is already in
+  use. The easy fix is to remove the superfluous name.
+
 Potential sources of incompatibilities between Coq V8.5 and V8.6
 ----------------------------------------------------------------
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 556df6e559..15cef676e6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2395,6 +2395,29 @@ let rec explicit_intro_names = function
      explicit_intro_names l
 | [] -> []
 
+let rec check_name_unicity env ok seen = function
+| (_, IntroForthcoming _) :: l -> check_name_unicity env ok seen l
+| (loc, IntroNaming (IntroIdentifier id)) :: l ->
+   (try
+      ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env);
+      user_err ~loc (pr_id id ++ str" is already used.")
+   with Not_found ->
+     if List.mem_f Id.equal id seen then
+       user_err ~loc (pr_id id ++ str" is used twice.")
+     else
+       check_name_unicity env ok (id::seen) l)
+| (_, IntroAction (IntroOrAndPattern l)) :: l' ->
+    let ll = match l with IntroAndPattern l -> [l] | IntroOrPattern ll -> ll in
+    List.iter (fun l -> check_name_unicity env ok seen (l@l')) ll
+| (_, IntroAction (IntroInjection l)) :: l' ->
+    check_name_unicity env ok seen (l@l')
+| (_, IntroAction (IntroApplyOn (c,pat))) :: l' ->
+    check_name_unicity env ok seen (pat::l')
+| (_, (IntroNaming (IntroAnonymous | IntroFresh _)
+     | IntroAction (IntroWildcard | IntroRewrite _))) :: l ->
+     check_name_unicity env ok seen l
+| [] -> ()
+
 let wild_id = Id.of_string "_tmp"
 
 let rec list_mem_assoc_right id = function
@@ -2530,13 +2553,21 @@ and prepare_intros_loc loc with_evars dft destopt = function
   | IntroForthcoming _ -> user_err ~loc 
       (str "Introduction pattern for one hypothesis expected.")
 
+let intro_patterns_head_core with_evars b destopt bound pat =
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let env = Proofview.Goal.env gl in
+    check_name_unicity env [] [] pat;
+    intro_patterns_core with_evars b [] [] [] destopt
+      bound 0 (fun _ l -> clear_wildcards l) pat
+  end }
+
 let intro_patterns_bound_to with_evars n destopt =
-  intro_patterns_core with_evars true [] [] [] destopt
-    (Some (true,n)) 0 (fun _ l -> clear_wildcards l)
+  intro_patterns_head_core with_evars true destopt
+    (Some (true,n))
 
 let intro_patterns_to with_evars destopt =
-  intro_patterns_core with_evars (use_bracketing_last_or_and_intro_pattern ())
-    [] [] [] destopt None 0 (fun _ l -> clear_wildcards l)
+  intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ())
+    destopt None
 
 let intro_pattern_to with_evars destopt pat =
   intro_patterns_to with_evars destopt [dloc,pat]
@@ -4191,6 +4222,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
       let f (_,is_not_let,_,_) = is_not_let in
       Array.map (fun (_,l) -> List.map f l) indsign in
     let names = compute_induction_names branchletsigns names in
+    Array.iter (check_name_unicity env toclear []) names;
     let tac =
     (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
       (Tacticals.New.tclTHENLIST [
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 239edd1da3..19c9fc4423 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 a7c497cfaf..9a5edb813d 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 ?].
-- 
cgit v1.2.3