[ssr] extended intro patterns: + > [^] /ltac:

This commit implements the following intro patterns:

Temporary "=> +"
 "move=> + stuff" ==== "move=> tmp stuff; move: tmp"
 It preserves the original name.
 "=>" can be chained to force generalization as in
 "move=> + y + => x z"

Tactics as views "=> /ltac:(tactic)"
 Supports notations, eg "Notation foo := ltac:(bla bla bla). .. => /foo".
 Limited to views on the right of "=>", views that decorate a tactic
 as move or case are not supported to be tactics.

Dependent "=> >H"
 move=> >H  ===== move=> ???? H, with enough ? to
 name H the first non-dependent assumption (LHS of the first arrow).
 TC isntances are skipped.

Block intro "=> [^ H] [^~ H]"
 after "case" or "elim" or "elim/v" it introduces in one go
 all new assumptions coming from the eliminations. The names are
 picked from the inductive type declaration or the elimination principle
 "v" in "elim/v" and are appended/prepended the seed "H"

The implementation makes crucial use of the goal_with_state feature of
the tactic monad. For example + schedules a generalization to be performed
at the end of the intro pattern and [^ .. ] reads the name seeds from
the state (that is filled in by case and elim).

0 files changed, 0 insertions, 0 deletions