diff --git a/src/g_ltac_iter.ml4 b/src/g_ltac_iter.ml4 index 6cafa0a..d080aec 100644 --- a/src/g_ltac_iter.ml4 +++ b/src/g_ltac_iter.ml4 @@ -70,10 +70,14 @@ struct | Reverse c -> resolve_collection (not reverse) c | HintDb db_name -> let db = - let syms = ref [] in - let db = Hints.searchtable_map db_name in - Hints.Hint_db.iter (fun _ _ hl -> syms := hl :: !syms) db ; - !syms + try + let db = Hints.searchtable_map db_name in + let syms = ref [] in + Hints.Hint_db.iter (fun _ _ hl -> syms := hl :: !syms) db ; + !syms + with Not_found -> + let _ = Tacticals.tclIDTAC_MESSAGE Pp.(str "Hint database " ++ str db_name ++ str " not found!") in + [] in if reverse then Proofview.Goal.nf_enter begin fun gl -> diff --git a/test-suite/example.v b/test-suite/example.v index 6794119..1e89a5a 100644 --- a/test-suite/example.v +++ b/test-suite/example.v @@ -39,4 +39,9 @@ Goal False -> True -> 1 = 1 -> True. let k l := pose l in foreach [ rev *|- ] k. exact I. -Defined. \ No newline at end of file +Defined. + +Goal True. + foreach [ db:does_not_exist ] ltac:(fun x => idtac x). + exact I. +Defined.