diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:38:36 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-15 10:38:36 +0200 |
commit | d2406149554812a01ac615af43af6b7b2a3efd72 (patch) | |
tree | 76879d5b7324f50ac482627bd4726496e70d6e24 /tactics | |
parent | 633b61e7ce82362a5c01724aa54b0e99dcfbb3ab (diff) | |
parent | f18899066d7c9185cfd131cae75d076c8b2a5e01 (diff) |
Merge PR #1046: Better error messages, fix for BZ#5723
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/hints.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index a572508d4..3ccbab874 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 () } |