diff options
| author | Samuel Gruetter | 2021-04-07 21:02:10 -0400 |
|---|---|---|
| committer | Samuel Gruetter | 2021-04-07 21:02:10 -0400 |
| commit | fb63ec7c10076d156caa43f73bad4f69653862a6 (patch) | |
| tree | 8311e352a1556d7b876ea1cbdde87ce538c7f9a7 /user-contrib/Ltac2/Notations.v | |
| parent | 59d0462f35818c12a0727a560d7b9ecf2ceea994 (diff) | |
unify for Ltac2
Fixes #14083
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). |