I agree, hence my qualification that it relies on an imperative layer (Ltac) to do anything useful, like dependent pattern-matching. I've edited my potentially ambiguous phrasing.