diff options
| -rw-r--r-- | src/tac2stdlib.ml | 7 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 10 | ||||
| -rw-r--r-- | src/tac2tactics.mli | 4 | ||||
| -rw-r--r-- | theories/Std.v | 2 |
4 files changed, 14 insertions, 9 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index ed0e6aafd3..b64aac3559 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -665,10 +665,9 @@ let () = define_prim4 "tac_newauto" begin fun bt dbg n lems dbs -> Tac2tactics.new_auto dbg n lems dbs end -let () = define_prim4 "tac_typeclasses_eauto" begin fun bt b str n dbs -> - let b = Value.to_bool b in +let () = define_prim3 "tac_typeclasses_eauto" begin fun bt str n dbs -> let str = to_strategy str in let n = Value.to_option Value.to_int n in - let dbs = Value.to_list Value.to_ident dbs in - Tac2tactics.typeclasses_eauto b str n dbs + let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in + Tac2tactics.typeclasses_eauto str n dbs end 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 diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli index 4369919d31..e0cd77096b 100644 --- a/src/tac2tactics.mli +++ b/src/tac2tactics.mli @@ -97,5 +97,5 @@ val new_auto : Hints.debug -> int option -> constr tactic list -> val eauto : Hints.debug -> int option -> int option -> constr tactic list -> Id.t list option -> unit Proofview.tactic -val typeclasses_eauto : bool -> Class_tactics.search_strategy -> int option -> - Id.t list -> unit Proofview.tactic +val typeclasses_eauto : Class_tactics.search_strategy -> int option -> + Id.t list option -> unit Proofview.tactic diff --git a/theories/Std.v b/theories/Std.v index b667258aa2..5201fa819d 100644 --- a/theories/Std.v +++ b/theories/Std.v @@ -226,4 +226,4 @@ Ltac2 @ external new_auto : debug -> int option -> (unit -> constr) list -> iden Ltac2 @ external eauto : debug -> int option -> int option -> (unit -> constr) list -> ident list option -> unit := "ltac2" "tac_eauto". -Ltac2 @ external typeclasses_eauto : bool -> strategy -> int option -> ident list -> unit := "ltac2" "tac_typeclasses_eauto". +Ltac2 @ external typeclasses_eauto : strategy -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto". |