----------------------------------------------------------------------
VALID_LT                                                    (Tactical)
----------------------------------------------------------------------
VALID_LT : list_tactic -> list_tactic

SYNOPSIS
Makes a list-tactic fail if it would otherwise return an invalid proof.

DESCRIBE
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 should produce a list {thl}
of theorems which are the goals {gl}, proved.

Precisely, for each goal {(asl, g)} in {gl}, the corresponding theorem in {thl}
should be {A |- g}, with {A} a subset of {asl}.
If this is not the case, then the list-tactic is invalid,
and {VALID_LT ltac gl} fails (raises an exception).
Otherwise, {VALID_LT ltac gl} behaves the same as {ltac gl}.

FAILURE
{VALID_LT ltac gl} fails by design if {ltac gl} produces new goals and
justification which do not prove the given goals {gl}.
Also fails if its {ltac gl} fails.

SEEALSO
Tactical.VALID, Tactical.VALIDATE_LT, proofManagerLib.elt,
proofManagerLib.expand_list.

----------------------------------------------------------------------