The Coq mailing list

[St�phane Lescuyer <lescuyer AT lri.fr>]

OK, thank you for your answer !

S.L.

2009/4/5  
<hugo.herbelin AT 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
>
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06