From 70187829867cfc19ec6ee5372e3c5f020fbf604e Mon Sep 17 00:00:00 2001 From: Armaël Guéneau Date: Tue, 29 May 2018 11:29:39 +0200 Subject: Fix anomaly in autoapply when an unbound hint name is provided --- tactics/class_tactics.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'tactics') diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3e08c6d87..d30f0b80b 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1229,8 +1229,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 -- cgit v1.2.3