make sure that 'in' clauses for reduction tactics are translated

once again re-organize the way intro patterns are translated: there is now
only one kind of pattern that can be used for both and and or constructs:
the use of the multiplet notation should only be a matter of notation.

un-capitalize a few tactic names for tactics represented using the TacExtend
construct.

corrects a bug in the way binders or coercion binders were used.


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

0 files changed, 0 insertions, 0 deletions