From eae015fa8aadab229a056eb869e2b926fa6c9dc2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 10 Nov 2020 15:14:11 +0100
Subject: Avoid exposing an internal names when "intros _ H" fails.

---
 tactics/tactics.ml            | 16 ++++++++++------
 test-suite/output/Tactics.out |  2 ++
 test-suite/output/Tactics.v   |  8 ++++++++
 3 files changed, 20 insertions(+), 6 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f3ecc2a9f0..e3369bc9be 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -198,22 +198,24 @@ let clear_in_global_msg = function
   | Some ref -> str " implicitly in " ++ Printer.pr_global ref
 
 let clear_dependency_msg env sigma id err inglobal =
+  let ppidupper = function Some id -> Id.print id | None -> str "This variable" in
+  let ppid = function Some id -> Id.print id | None -> str "this variable" in
   let pp = clear_in_global_msg inglobal in
   match err with
   | Evarutil.OccurHypInSimpleClause None ->
-      Id.print id ++ str " is used" ++ pp ++ str " in conclusion."
+      ppidupper id ++ str " is used" ++ pp ++ str " in conclusion."
   | Evarutil.OccurHypInSimpleClause (Some id') ->
-      Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
+      ppidupper id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"."
   | Evarutil.EvarTypingBreak ev ->
-      str "Cannot remove " ++ Id.print id ++
+      str "Cannot remove " ++ ppid id ++
       strbrk " without breaking the typing of " ++
       Printer.pr_existential env sigma ev ++ str"."
   | Evarutil.NoCandidatesLeft ev ->
-      str "Cannot remove " ++ Id.print id ++ str " as it would leave the existential " ++
+      str "Cannot remove " ++ ppid id ++ str " as it would leave the existential " ++
       Printer.pr_existential_key sigma ev ++ str" without candidates."
 
 let error_clear_dependency env sigma id err inglobal =
-  user_err (clear_dependency_msg env sigma id err inglobal)
+  user_err (clear_dependency_msg env sigma (Some id) err inglobal)
 
 let replacing_dependency_msg env sigma id err inglobal =
   let pp = clear_in_global_msg inglobal in
@@ -2130,7 +2132,9 @@ let clear_body ids =
   end
 
 let clear_wildcards ids =
-  Tacticals.New.tclMAP (fun {CAst.loc;v=id} -> clear [id]) ids
+  let clear_wildcards_msg ?loc env sigma _id err inglobal =
+    user_err ?loc (clear_dependency_msg env sigma None err inglobal) in
+  Tacticals.New.tclMAP (fun {CAst.loc;v=id} -> clear_gen (clear_wildcards_msg ?loc) [id]) ids
 
 (*   Takes a list of booleans, and introduces all the variables
  *  quantified in the goal which are associated with a value
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 70427220ed..3f07261ca6 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -7,3 +7,5 @@ H is already used.
 The command has indeed failed with message:
 H is already used.
 a
+The command has indeed failed with message:
+This variable is used in hypothesis H.
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index 96b6d652c9..8526e43a23 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -30,3 +30,11 @@ Goal True.
   assert_succeeds should_not_loop.
   assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
 Abort.
+
+Module IntroWildcard.
+
+Theorem foo : { p:nat*nat & p = (0,0) } -> True.
+Fail intros ((n,_),H).
+Abort.
+
+End IntroWildcard.
-- 
cgit v1.2.3