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

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 ?].