git.iko.soy/Idris-dev
on master help sign in
Remove deprecated functions from Language.Reflection.
678f590Jan de Muijnck-Hughes
libs/prelude/Language/Reflection.idr+1−9
compare with master
unifiedsplit
@@ -74,14 +74,6 @@ mutual
74 | MetaN TTName TTName
74 | MetaN TTName TTName
75 %name SpecialName sn, sn'
75 %name SpecialName sn, sn'
76
76
77−InstanceN : TTName -> (List String) -> SpecialName
78−InstanceN = ImplementationN
79−%deprecate InstanceN "`InstanceN` is deprecated, Please use `ImplementationN` instead."
80−
81−InstanceCtorN : TTName -> SpecialName
82−InstanceCtorN = ImplementationCtorN
83−%deprecate InstanceCtorN "`InstanceCtorN` is deprecated, Please use `ImplementationCtorN` instead."
84−
85-- Rather than implement one-off private functions, we make the
77-- Rather than implement one-off private functions, we make the
86-- disjointness of the constructors available to all Idris programs,
78-- disjointness of the constructors available to all Idris programs,
87-- at the cost of a bit of scrolling here.
79-- at the cost of a bit of scrolling here.
@@ -410,7 +402,7 @@ mutual
410 private
402 private
411 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
403 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
412 implementationNInj Refl = (Refl, Refl)
404 implementationNInj Refl = (Refl, Refl)
413−
405+
414 private
406 private
415 parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)
407 parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)
416 parentNInj Refl = (Refl, Refl)
408 parentNInj Refl = (Refl, Refl)
libs/prelude/Language/Reflection/Elab.idr−6
@@ -560,11 +560,6 @@ namespace Tactics
560 addImplementation : (ifaceName, implName : TTName) -> Elab ()
560 addImplementation : (ifaceName, implName : TTName) -> Elab ()
561 addImplementation ifaceName implName = Prim__AddImplementation ifaceName implName
561 addImplementation ifaceName implName = Prim__AddImplementation ifaceName implName
562
562
563− export
564− addInstance : (ifaceName, implName : TTName) -> Elab ()
565− addInstance = addImplementation
566− %deprecate addInstance "`addInstance` is deprecated, Please use `addImplementation` instead."
567−
568 ||| Determine whether a name denotes an interface.
563 ||| Determine whether a name denotes an interface.
569 |||
564 |||
570 ||| @ name a name that might denote an interface.
565 ||| @ name a name that might denote an interface.
@@ -769,4 +764,3 @@ implementation Quotable Datatype Raw where
769 quotedTy = `(Datatype)
764 quotedTy = `(Datatype)
770 quote (MkDatatype name tyConArgs tyConRes constructors) =
765 quote (MkDatatype name tyConArgs tyConRes constructors) =
771 `(MkDatatype ~(quote name) ~(quote tyConArgs) ~(quote tyConRes) ~(quote constructors))
766 `(MkDatatype ~(quote name) ~(quote tyConArgs) ~(quote tyConRes) ~(quote constructors))
772−