Extend ElimModal with Boolean flags to specify whether it operates on the…

Extend ElimModal with Boolean flags to specify whether it operates on the persistent/spatial context:

Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
  elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.

This provides a preparation for #167.