diff options
Diffstat (limited to 'user-contrib/Ltac2/Notations.v')
| -rw-r--r-- | user-contrib/Ltac2/Notations.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v index 931d753521..77531121cb 100644 --- a/user-contrib/Ltac2/Notations.v +++ b/user-contrib/Ltac2/Notations.v @@ -593,6 +593,8 @@ 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. + (** Congruence *) Ltac2 f_equal0 () := ltac1:(f_equal). |