aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-07 13:01:23 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-07 13:01:23 +0200
commit28ca5295339afecfc4ecb70214f6f575c11e34a1 (patch)
tree6b18213b73d03e5888c39685416bccd80adc35a6
parentf2b28f819c16ad773ab5a2e426e3c0a478cbfdef (diff)
parent70187829867cfc19ec6ee5372e3c5f020fbf604e (diff)
Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is provided
-rw-r--r--tactics/class_tactics.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c105116ff..4beeaaae0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1206,8 +1206,11 @@ let is_ground c =
let autoapply c i =
let open Proofview.Notations in
Proofview.Goal.enter begin fun gl ->
+ let hintdb = try Hints.searchtable_map i with Not_found ->
+ CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ "."))
+ in
let flags = auto_unif_flags Evar.Set.empty
- (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
+ (Hints.Hint_db.transparent_state hintdb) in
let cty = Tacmach.New.pf_unsafe_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
unify_e_resolve false flags gl