diff options
| -rw-r--r-- | src/tac2stdlib.ml | 2 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 2 | ||||
| -rw-r--r-- | src/tac2tactics.mli | 2 | ||||
| -rw-r--r-- | theories/Notations.v | 4 | ||||
| -rw-r--r-- | theories/Std.v | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml index b64aac3559..a0eb0d60e5 100644 --- a/src/tac2stdlib.ml +++ b/src/tac2stdlib.ml @@ -666,7 +666,7 @@ let () = define_prim4 "tac_newauto" begin fun bt dbg n lems dbs -> end let () = define_prim3 "tac_typeclasses_eauto" begin fun bt str n dbs -> - let str = to_strategy str in + let str = Value.to_option to_strategy str in let n = Value.to_option Value.to_int n in let dbs = Value.to_option (fun l -> Value.to_list Value.to_ident l) dbs in Tac2tactics.typeclasses_eauto str n dbs diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index 6cf8f24f27..447f602f7a 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -251,4 +251,4 @@ let typeclasses_eauto strategy depth dbs = let dbs = List.map Id.to_string dbs in false, dbs in - Class_tactics.typeclasses_eauto ~only_classes ~strategy ~depth dbs + Class_tactics.typeclasses_eauto ~only_classes ?strategy ~depth dbs diff --git a/src/tac2tactics.mli b/src/tac2tactics.mli index e0cd77096b..78d421303a 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 : Class_tactics.search_strategy -> int option -> +val typeclasses_eauto : Class_tactics.search_strategy option -> int option -> Id.t list option -> unit Proofview.tactic diff --git a/theories/Notations.v b/theories/Notations.v index e7fc43c0ee..5fdb4ec8af 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -491,10 +491,10 @@ Ltac2 Notation "eauto" n(opt(tactic(0))) p(opt(tactic(0))) Ltac2 Notation eauto := eauto. Ltac2 Notation "typeclasses_eauto" n(opt(tactic(0))) - dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto Std.DFS n dbs. + dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto None n dbs. Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0))) - dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto Std.BFS n dbs. + dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto (Some Std.BFS) n dbs. Ltac2 Notation typeclasses_eauto := typeclasses_eauto. diff --git a/theories/Std.v b/theories/Std.v index 79a7be1d63..b63c2eaa41 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 : strategy -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto". +Ltac2 @ external typeclasses_eauto : strategy option -> int option -> ident list option -> unit := "ltac2" "tac_typeclasses_eauto". |