From f18899066d7c9185cfd131cae75d076c8b2a5e01 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 11 Sep 2017 14:30:48 -0400
Subject: Better error messages, fix for BZ#5723

---
 tactics/hints.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index a572508d47..3ccbab874f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -56,7 +56,9 @@ let head_constr_bound sigma t =
   | _ -> raise Bound
 
 let head_constr sigma c =
-  try head_constr_bound sigma c with Bound -> user_err Pp.(str "Bound head variable.")
+  try head_constr_bound sigma c
+  with Bound -> user_err (Pp.str "Head identifier must be a constant, section variable, \
+                                  (co)inductive type, (co)inductive type constructor, or projection.")
 
 let decompose_app_bound sigma t =
   let t = strip_outer_cast sigma t in
@@ -764,7 +766,9 @@ let rec nb_hyp sigma c = match EConstr.kind sigma c with
 
 let try_head_pattern c =
   try head_pattern_bound c
-  with BoundPattern -> user_err Pp.(str "Bound head variable.")
+  with BoundPattern ->
+    user_err (Pp.str "Head pattern or sub-pattern must be a global constant, a section variable, \
+                      an if, case, or let expression, an application, or a projection.")
 
 let with_uid c = { obj = c; uid = fresh_key () }
 
-- 
cgit v1.2.3