The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Ian,

 it’s an overlook or maybe it can’t be done easily. Have a look at 
Program/Equality.v for the definitions of dependent destruction/induction.
You just need to tweak the [fun hyp => destruct …) part. I’m just not
sure one can make tactic notations that take intro patterns out of the box.

Tactic Notation "dependent" "destruction" ident(H) := 
  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => do_case hyp) H.

Tactic Notation "dependent" "destruction" ident(H) "using" constr(c) := 
  do_depelim' ltac:(fun hyp => idtac) ltac:(fun hyp => destruct hyp using c) 
H.

Best,
— Matthieu

On 27 déc. 2013, at 13:46, Ian Lynagh 
<igloo AT earth.li>
 wrote:

> 
> Hi all,
> 
> I would like to write "dependent destruction ... as ...", but it seems
> that this does not exist. "dependent inversion ... as ..." does exist,
> but when using dependent inversion I get "Error: Current goal does not
> depend on H".
> 
> Is there any way to do what dependent destruction does, but to name the
> things that are created while doing so?
> 
> I have Coq 8.4pl3 (December 2013).
> 
> 
> Thanks
> Ian
>