Added select and select_revert tactics

As discussed with @robbertkrebbers open points:

• Names of the tactics (What are the names in Mtac? @janno )
• Changelog entry?

theories/tactics.v

@@ -520,6 +520,20 @@ Ltac find_pat pat tac :=
       tryif tac x then idtac else fail 2
   end.
 
+
+(** [select] finds the first hypothesis matching [pat] and passes it
+to the continuation [tac]. It's main advantage over using [match goal
+with ] directly is that it is shorter. This tactic does not backtrack
+if [tac] fails or in case of ambiguous matches. *)
+Tactic Notation "select" open_constr(pat) tactic(tac) :=
+  lazymatch goal with
+  (* The unify is necessary, otherwise holes in p stay as sideconditions *)
+  | H : pat |- _ => let T := (type of H) in unify T pat; tac H
+  end.
+(** [select_revert] reverts the first hypothesis matching [pat] and
+reverts it. *)
+Tactic Notation "revert" "select" open_constr(pat) := select pat (fun H => revert H).
+
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
 to solve propositions on sets. The [naive_solver] tactic implements an