@@ -255,10 +255,10 @@ instance forall k p
255 h :: DSum k (ToFrom k p) -> [DSum k (Const (Fixup k p))]
255 h :: DSum k (ToFrom k p) -> [DSum k (Const (Fixup k p))]
256 h ((between :: k between) :=> ToFrom editAfter editBefore) = case (editAfter, editBefore) of
256 h ((between :: k between) :=> ToFrom editAfter editBefore) = case (editAfter, editBefore) of
257 (To_Move (Some (toAfter :: k after)), From_Move ((fromBefore :: k before) :=> Flip p) :: From k p between) ->
257 (To_Move (Some (toAfter :: k after)), From_Move ((fromBefore :: k before) :=> Flip p) :: From k p between) ->
258− case toAfter `geq` fromBefore of
259− Just Refl | Just Refl <- Cat.isId p ->
258+ case Cat.isId p of
260 [ toAfter :=> Const Fixup_Delete ]
260 [ toAfter :=> Const Fixup_Delete ]
262 [ toAfter :=> Const (Fixup_Update $ This $ between :=> From_Move (fromBefore :=> Flip p))
262 [ toAfter :=> Const (Fixup_Update $ This $ between :=> From_Move (fromBefore :=> Flip p))
263 , fromBefore :=> Const (Fixup_Update $ That $ To_Move $ Some toAfter)
263 , fromBefore :=> Const (Fixup_Update $ That $ To_Move $ Some toAfter)