Behaviour change for Force/Delay in Idris 0.99? (Section 11.1.4, MEAP v13)

In the implementation for getPrefix in section 11.1.4 in step 4, you show the following hole:

  a : Type
  k : Nat
  value : a
  xs : Inf (InfList a)
--------------------------------------
getPrefix_rhs_1 : List a

… and finish the implementation with the clause

getPrefix (S k) (value :: xs) = value :: getPrefix k (Force xs)

However, this is not what I'm seeing in Idris 0.99. The Inf has already been removed and I don't need a Force:

- + Main.getPrefix_rhs_1 [P]
 `--                     a : Type
                         k : Nat
                     value : a
                        xs : InfList a
     ----------------------------------
      Main.getPrefix_rhs_1 : List a

The next section talks about how Idris will implicitly insert Delay and Force for you. Has any of this behaviour changed between 0.12 and 0.99?

Here's the complete code:

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : (count : Nat) -> InfList a -> List a
getPrefix Z _ = []
getPrefix (S k) (value :: xs) = ?getPrefix_rhs_1