The Coq mailing list

[Jianzhou Zhao <jianzhou AT seas.upenn.edu>]

Hello,

I wanted to define a tactical working like
  destruct H as J1 J2 ...
The list of names of J's is with variant length.  I defined:

Ltac destructn H Js :=
  match Js with
  | nil => idtac
  | ?J::nil => rename H into J
  | ?J::?Js' => destruct H as [H J]; bdestructn H Js
  end.

But I failed to figure out how to give a list of Js,
  destructn H (J1::J2::nil)
doesn't work, because J1 J2 are not in the current context.

Is there any syntax like ident(...) in 'Tactic Notation'  to tell Coq
that J1 and J2 are used as identifiers under Ltac? or I should do
anything else?

Thanks a lot.
-- 
Jianzhou