The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi,

> I was trying to use  the new hyp_list and ne_hyp_list argument types
> of Tactic Notations:
> 
> Tactic Notation "mytactic" hyp_list(Hyps) :=
>   ....
> 
> I can't find a way to deconstruct or traverse these lists in the body
> of the tactic; therefore it seems the only thing that one can do is to
> pass this list of hypotheses
> to an existing tactic awaiting a list of arguments (clean, revert, ...
> ; idtac will not print the list though). Can anyone confirm this ?

Nothing is indeed provided to deconstruct or traverse these lists. As
Coq is, one can only use them in tactics awaiting for list of
arguments. Regarding idtac, it could indeed print the actual
list and this will be considered.

Hugo Herbelin