diff options
Diffstat (limited to 'src/tac2tactics.ml')
| -rw-r--r-- | src/tac2tactics.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index b35e26c89e..6cf8f24f27 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -243,6 +243,12 @@ let eauto debug n p lems dbs = let dbs = Option.map (fun l -> List.map Id.to_string l) dbs in Eauto.gen_eauto (Eauto.make_dimension n p) lems dbs -let typeclasses_eauto only_classes strategy depth dbs = - let dbs = List.map Id.to_string dbs in +let typeclasses_eauto strategy depth dbs = + let only_classes, dbs = match dbs with + | None -> + true, [Hints.typeclasses_db] + | Some dbs -> + let dbs = List.map Id.to_string dbs in + false, dbs + in Class_tactics.typeclasses_eauto ~only_classes ~strategy ~depth dbs |