Revert patterns

We implement : tactical, which behaves in a similar way as it does in SSReflect. tac: r_1 r_2 .. r_n will revert all r_is back to the goal and then executes tactic tac.

1. : r: if r is a hypothesis in a local, will revert r and all hypothesis depended on it.
2. : (r): if r is a term with wholes, it will abstract the goal over it and revert it to the goal stack
3. : [r_i]: if r_i is a term of type Prop and is decidable, it will abstract the goal over Decidable r and revert the decidable instance to the goal stack. This is useful for true/false case analysis on the decidable proposition. For instance:

scase: [i ∈ l]

will transform goal ?goal in to two goals: i ∈ l -> ?goal and i ∉ l -> ?goal

4. : {a1 .. an}: erases ai from the local context