Fix caml debug flags configuration, -g works with the native compiler only

since 3.10. Fix a bug in classes when the instance database is empty.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10945 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 1 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 00f8179ca..618d48482 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -359,7 +359,12 @@ let full_eauto debug n lems gls =
 
 let typeclasses_eauto debug n lems gls = 
   let dbnames = [typeclasses_db] in
-  let db_list = List.map searchtable_map dbnames in
+  let db_list = List.map
+    (fun x -> 
+      try searchtable_map x 
+      with Not_found -> (empty_transparent_state, Hint_db.empty))
+    dbnames 
+  in
     e_search_auto debug n lems db_list gls
 
 exception Found of evar_map