Library Ltac2.Ltac1CompatNotations



Require Import Ltac2.Init Ltac2.Std.

Ltac2 Notation "transitivity" c(constr) := Std.transitivity c.