Can't use %runElab in 'let ... in' statement

[Pytheas01]

Hello, if you cut and paste the second Elab proof displayed at the bottom of the Automatic Theorem Proving documentation (http://docs.idris-lang.org/en/latest/proofs/interactive.html), into the second 'hole' in the example code, an error message stating that "in" is "unexpected" is displayed.

Steps to Reproduce

import Pruviloj
import Pruviloj.Induction

%language ElabReflection

plusReducesZ' : (n:Nat) -> n = plus n Z
plusReducesZ' Z = %runElab (do reflexivity)
plusReducesZ' (S k) = let ih = plusReducesZ' k in
                        %runElab (do intro `{{k}}
                                    intro `{{ih}}
                                    compute
                                    rewriteWith (Var `{{ih}})
                                    reflexivity)

Expected Behavior

The compiler should not generate any errors (cf. "Again, we can cut & paste this into the hole in the original file." statement at the bottom of the aforementioned documentation page).

Observed Behavior

16 | intro `{{ih}} | ^ unexpected "in" expecting dependent type signature

[Pytheas01]

NB : the 'compute' command should be removed in the source code above