diff options
Diffstat (limited to 'user-contrib/Ltac2/Notations.v')
| -rw-r--r-- | user-contrib/Ltac2/Notations.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v index 77531121cb..6ddad8f1c9 100644 --- a/user-contrib/Ltac2/Notations.v +++ b/user-contrib/Ltac2/Notations.v @@ -593,7 +593,7 @@ Ltac2 Notation "typeclasses_eauto" "bfs" n(opt(tactic(0))) Ltac2 Notation typeclasses_eauto := typeclasses_eauto. -Ltac2 Notation "unify" x(constr) y(constr) db(opt(seq("with", ident))) := Std.unify x y db. +Ltac2 Notation "unify" x(constr) y(constr) := Std.unify x y. (** Congruence *) |