diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-11-26 17:32:01 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-11-26 17:32:01 +0100 |
| commit | 22c3951cfdf4938fa6df7368daed7bead05e4592 (patch) | |
| tree | 21c3ea90d39bc40f387beefeb455d9933a596d58 /CHANGES | |
| parent | 47e2b3bbf10a391a4131697f202991470c9a68de (diff) | |
A shortcut for coq-insert-as-in-next-command.
Works well for a single induction/destruct.
Works sometimes for inversion.
Does not work in presence of eqn flag yet (easy to fix).
Does not work on ;-combined tactics (hard to fix).
Does not work on a lot of inversion invocation (but some are ok).
We basically need another "as" tactical with a retro-predictable input.
That is: when seeing the resulting goal we can deduce what would have
been the right "as" close. This is currently the case only for
destruct/induction !foo (notice the exclamation mark).
Diffstat (limited to 'CHANGES')
0 files changed, 0 insertions, 0 deletions