diff options
| author | Pierre-Marie Pédrot | 2017-09-05 01:07:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-05 01:07:04 +0200 |
| commit | 9a3853fe872e200ed1b34319f6ff0f85a171a434 (patch) | |
| tree | 5ef7e1f5509fc46baf7dc03a5a7ca3b2cca2530a | |
| parent | da28b6e65d9b9a74c277cb15055131c8a151bb72 (diff) | |
Fixup grammar of typeclasses_eauto.
| -rw-r--r-- | theories/Notations.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Notations.v b/theories/Notations.v index 4cb4f32682..e7fc43c0ee 100644 --- a/theories/Notations.v +++ b/theories/Notations.v @@ -490,10 +490,10 @@ Ltac2 Notation "eauto" n(opt(tactic(0))) p(opt(tactic(0))) Ltac2 Notation eauto := eauto. -Ltac2 Notation "typeclasses_eauto" n(opt(tactic(0))) p(opt(tactic(0))) +Ltac2 Notation "typeclasses_eauto" n(opt(tactic(0))) dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto Std.DFS n dbs. -Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0))) p(opt(tactic(0))) +Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0))) dbs(opt(seq("with", list1(ident)))) := Std.typeclasses_eauto Std.BFS n dbs. Ltac2 Notation typeclasses_eauto := typeclasses_eauto. |