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...

tests/tactics.ref

+The command has indeed failed with message:
+Failed to progress.
+The command has indeed failed with message:
+Ltac call to "destruct_or !" failed.
+Failed to progress.
+The command has indeed failed with message:
+Ltac call to "destruct_and !" failed.
+Failed to progress.