substs and reflexivity

Stream: general

[Sean Leather]

It seems like subst solves a reflexive goal but substs does not. If I replace subst p, subst qwith substs p q, I have to add refl to solve the goal.

Looking at the definition of the interactive subst, I can see why:

meta def subst (q : parse texpr) : tactic unit :=
i_to_expr q >>= tactic.subst >> try (tactic.reflexivity reducible)

So the documentation on substs is not quite correct:

/-- Multiple subst. `substs x y z` is the same as `subst x, subst y, subst z`. -/
meta def substs (l : parse ident*) : tactic unit :=
l.mmap' (λ h, get_local h >>= tactic.subst)

Is it enough to add >> try (tactic.reflexivity reducible) to the end of the substs definition to recoup this feature? Is there any reason why we shouldn't do this?