Fixes and refinements regarding occurrence selection:

- make the modifiers "value of" and "type of" for "set" working (it was not!),
- clear unselected hypotheses in the "in" clause of "induction/destruct" when
  the destructed term is a variable (experimental),
- support for generalization of hypotheses in the induction hypotheses using
  the "in" clause of "induction" (e.g. "induction n in m, H" will
  generalize over m -- would it be better to have an explicit 
  "over"/"generalizing" clause ?).
Added clause "as" to "apply in".



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

0 files changed, 0 insertions, 0 deletions