diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Notations.v | 4 | ||||
| -rw-r--r-- | theories/Std.v | 2 |
2 files changed, 3 insertions, 3 deletions
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". |