Rewriting in the context fails only some times

[sarranz]

The following gives unknown lemma 'h1'

lemma ble foo :
  !foo =>
  foo =>
  false.
move=> h0 h1.
rewrite h1 in h0.

But if the rewrite is h0 in h1 it works.

[strub]

When rewriting in h0, only the context above h0 is accessible. This is to prevent to introduce new variables that would appear after the local hypothesis. One solution would be to move h0 to the end of the context, maybe with a varaition of the in meta-command.