Merge pull request #6 from gmalecha/no-anomoly

avoid anomolies when a hint database doesn't exist
gmalecha · Oct 15, 2019 · 63f26ea · 63f26ea
2 parents 77a33c9 + 746a99b
commit 63f26ea
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 5 deletions.
diff --git 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
@@ -39,4 +39,9 @@ Goal False -> True -> 1 = 1 -> True.
   let k l := pose l in
   foreach [ rev *|- ] k.
   exact I.
-Defined.
+Defined.
+
+Goal True.
+  foreach [ db:does_not_exist ] ltac:(fun x => idtac x).
+  exact I.
+Defined.