@@ -290,7 +290,7 @@ instance forall k p
290 f@(From_Move ((between0 :: k between0) :=> Flip (p' :: p between0 a))) -> case getHere u of -- The `from` fixup comes from the "old" patch
290 f@(From_Move ((between0 :: k between0) :=> Flip (p' :: p between0 a))) -> case getHere u of -- The `from` fixup comes from the "old" patch
291 Nothing -> f -- If there's no `from` fixup, just use the "new" `from`
291 Nothing -> f -- If there's no `from` fixup, just use the "new" `from`
292 Just ((between1 :: k between1) :=> frm) -> case geq between0 between1 of
292 Just ((between1 :: k between1) :=> frm) -> case geq between0 between1 of
293− Nothing -> error "fixup joined-on key did not match"
293+ Nothing -> error "PatchMapWithPatchingMove: fixup joined-on key did not match"
294 Just Refl -> case frm of
294 Just Refl -> case frm of
295 From_Insert v -> From_Insert $ applyAlwaysHet2 p' v
295 From_Insert v -> From_Insert $ applyAlwaysHet2 p' v
296 From_Delete -> From_Delete
296 From_Delete -> From_Delete