clean commented code

Author: EwenBC

src/Agda/Core/Name.agda

@@ -98,13 +98,3 @@ pattern V2suc n p = ⟨ _ ⟩ (Suc (Suc n) ⟨ IsSuc (IsSuc p) ⟩)
 pattern Vzero = ⟨ _ ⟩ Zero ⟨ IsZero refl ⟩
 pattern Vone = ⟨ _ ⟩ (Suc Zero) ⟨ IsSuc (IsZero refl) ⟩
 -------------------------------------------------------------------------------
-{-
-data CaseComparaison : NameIn α → NameIn α → Set where
-  GT : {x y : NameIn α} → @0 {{x ≡ Vzero }} → CaseComparaison x y
-  EQ : {x y : NameIn α} → compare x y ≡ EQ → CaseComparaison x y
-  LT : {x y : NameIn α} → compare x y ≡ LT → CaseComparaison x y
-
-
-caseCompare : (x y : NameIn α) → CaseComparaison x y
-caseCompare = ?
--- -}

src/Agda/Core/ScopeUtils.agda

@@ -37,16 +37,4 @@ module Shrink where
     SubToShrink βRun (⟨ γ ⟩ EmptyR) = idShrink βRun
     SubToShrink βRun (⟨ γ ⟩ ConsL x p) = ShKeep x (SubToShrink (rezzUnbind βRun) < p >)
     SubToShrink βRun (⟨ γ ⟩ ConsR y p) = ShCons y (SubToShrink (rezzUnbind βRun) < p >)
-  {-
-  opaque
-    unfolding Sub Split SubToShrink splitEmptyLeft
-    ShrinkEquivLeft : (βRun : Rezz β) (s : Shrink α β) → SubToShrink βRun (ShrinkToSub s) ≡ s
-    ShrinkEquivLeft βRun ShNil = refl
-    ShrinkEquivLeft βRun (ShKeep x s) = do
-      let e = ShrinkEquivLeft (rezzUnbind βRun) s
-      subst (λ z → SubToShrink βRun (ShrinkToSub (ShKeep x s)) ≡ ShKeep x z ) e {!   !}
-    ShrinkEquivLeft βRun (ShCons x s) = do
-      let e = ShrinkEquivLeft (rezzUnbind βRun) s
-      subst (λ z → SubToShrink βRun (ShrinkToSub (ShCons x s)) ≡ ShCons x z ) e {!   !}
-  -}
-{- End of module Shrink -}
+{- End of module Shrink -}