Add destruct_or tactics to (possibly repeatedly) split disjunctions in an assumption

Following split_and, the new tactics are split_or H, split_or? H and split_or! H. The name H is reused for the assumptions that are produced by destructing the disjunction (no fresh name is introduced).

I was pondering whether the tactic should be split_or H or split_or in H. The second one follows the usual pattern of in+assumption, but at the same time there is not going to be a split_or tactic that works on the goal, so...

theories/tactics.v

@@ -84,9 +84,9 @@ Tactic Notation "etrans" := etransitivity.
 (** Tactics for splitting conjunctions:
 
 - [split_and] : split the goal if is syntactically of the shape [_ ∧ _]
-- [split_ands?] : split the goal repeatedly (perhaps zero times) while it is
+- [split_and?] : split the goal repeatedly (perhaps zero times) while it is
   of the shape [_ ∧ _].
-- [split_ands!] : works similarly, but at least one split should succeed. In
+- [split_and!] : works similarly, but at least one split should succeed. In
   order to do so, it will head normalize the goal first to possibly expose a
   conjunction.
 
@@ -109,6 +109,24 @@ Tactic Notation "destruct_and" "?" :=
   end.
 Tactic Notation "destruct_and" "!" := progress (destruct_and?).
 
+(** Tactics for splitting disjunctions in an assumption:
+
+- [split_or H] : splits the assumption H if it is of the shape [_ ∨ _]
+- [split_or? H] : split the assumption H repeatedly (perhaps zero times)
+  while it is of the shape [_ ∨ _].
+- [split_or! H] : works similarly, but at least one split should succeed.
+  In order to do so, it will head normalize the goal first to possibly
+  expose a disjunction.
+*)
+
+Tactic Notation "split_or" ident(H) :=
+match goal with
+| H : _ ∨ _ |- _ => destruct H as [H|H]
+| H : Is_true (_ || _) |- _ => apply orb_True in H; destruct H as [H|H]
+end.
+Tactic Notation "split_or" "?" ident(H) := repeat (split_or H).
+Tactic Notation "split_or" "!" ident(H) := hnf in H; split_or H; split_or? H.
+
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used
 together with the [repeat] tactical. *)