GEN_VALIDATE_LT : bool -> list_tactic -> list_tactic
When list-tactic ltac is applied to a goal list gl it produces a new goal list gl' and a justification. When the justification is applied to a list thl' of theorems which are the new goals gl', proved, it produces a list thl of theorems (which, for a valid list-tactic are the goals gl, proved).
But GEN_VALIDATE_LT false ltac also returns extra subgoals corresponding to the assumptions of thl.
See GEN_VALIDATE for more details.
Also fails if ltac fails when applied to the given goals.