Added support for interpreting hyp lists in tactic notations.
Using an or_var rather than the hack with loc for coding a pure ident
as a disjunctive intropattern.