diff options
| author | Pierre-Marie Pédrot | 2017-09-05 01:29:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 01:29:47 +0200 |
| commit | 4a8399e62dd4bdf5876e714910dd2c7cb433dfda (patch) | |
| tree | 13b62ff5c9751f39daf7eb38f3ea21d20e47d961 /theories | |
| parent | 9a3853fe872e200ed1b34319f6ff0f85a171a434 (diff) | |
Typeclasses_eauto strategy is now optional.
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". |