@@ -404,9 +404,8 @@ mutual
404 withNInj Refl = (Refl, Refl)
404 withNInj Refl = (Refl, Refl)
407− instanceNInj : (InstanceN n xs = InstanceN n' ys) -> (n = n', xs = ys)
407+ instanceNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
408 instanceNInj Refl = (Refl, Refl)
408 instanceNInj Refl = (Refl, Refl)
409− %deprecate instanceNInj "`instanceNInj` is deprecated, Please use `implementationNInj` instead."
412 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
411 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
@@ -577,6 +576,9 @@ mutual
577 decSNEq (MetaN n n') (MetaN x y) | No contra =
576 decSNEq (MetaN n n') (MetaN x y) | No contra =
578 No $ contra . fst . metaNInj
577 No $ contra . fst . metaNInj
579+-- (Temporarily?) Outside the mutual block, since otherwise we get the
580+-- warning on the second pass!
581+%deprecate instanceNInj "`instanceNInj` is deprecated, Please use `implementationNInj` instead."
581implementation DecEq TTName where
583implementation DecEq TTName where
582 decEq = decTTNameEq
584 decEq = decTTNameEq