Made intros_until and onInductionArg a bit stricter and robust

The tolerance for overloading "id" as quantified hypothesis and as
declared variable is kept - because induction_arg entry is not
available to extended tactics, e.g. "discriminate", and these
extensions do not know a priori if a name is quantified or declared.

However, an upstream check is done to ensure that an induction
argument exists as term if not quantified so that the tactics do not
have to check this individually by themselves.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13125 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions