git.iko.soy/Idris-dev
on master help sign in
Remove deprecated functions from Language.Reflection.
commit678f590aabb4ead7d32d57cbfdd861685572d31b authorJan de Muijnck-Hughes <jan.deMuijnck-Hughes@glasgow.ac.uk> dateFri 10 Nov 2017, 11:15 (9 years ago) parentf80814a
2 files changed+1−15
compare with master
unifiedsplit
libs/prelude/Language/Reflection.idr+1−9 libs/prelude/Language/Reflection/Elab.idr−6
libs/prelude/Language/Reflection.idr+1−9
@@ -74,14 +74,6 @@ mutual
7474 | MetaN TTName TTName
7575 %name SpecialName sn, sn'
7676
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−
8577-- Rather than implement one-off private functions, we make the
8678-- disjointness of the constructors available to all Idris programs,
8779-- at the cost of a bit of scrolling here.
@@ -410,7 +402,7 @@ mutual
410402 private
411403 implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)
412404 implementationNInj Refl = (Refl, Refl)
413−
405+
414406 private
415407 parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)
416408 parentNInj Refl = (Refl, Refl)
libs/prelude/Language/Reflection/Elab.idr−6
@@ -560,11 +560,6 @@ namespace Tactics
560560 addImplementation : (ifaceName, implName : TTName) -> Elab ()
561561 addImplementation ifaceName implName = Prim__AddImplementation ifaceName implName
562562
563− export
564− addInstance : (ifaceName, implName : TTName) -> Elab ()
565− addInstance = addImplementation
566− %deprecate addInstance "`addInstance` is deprecated, Please use `addImplementation` instead."
567−
568563 ||| Determine whether a name denotes an interface.
569564 |||
570565 ||| @ name a name that might denote an interface.
@@ -769,4 +764,3 @@ implementation Quotable Datatype Raw where
769764 quotedTy = `(Datatype)
770765 quote (MkDatatype name tyConArgs tyConRes constructors) =
771766 `(MkDatatype ~(quote name) ~(quote tyConArgs) ~(quote tyConRes) ~(quote constructors))
772−