The Coq mailing list

[xiang sen <xiangsen AT ustc.edu>]

Pierre Casteran wrote:

> Selon xiang sen 
> <xiangsen AT ustc.edu>:
>
>  
>
> > Thanks.
> >
> > But what I want is matching several hypothesis,
> > because I need multi hypoth in the tac.
> > You mean, it's necessary to use "match .. match ..." instead of
> > "match goal with [h1: t1; h2 :t2;..|-C]"?
> >
> > I find in P.203 of Coq art that "The keywords "match goal with "
> > indicate that patterns are applied to match the goal. The patterns
> > have the form [h1 : t1; h2 : t2; ..|- C]=>tac". Why what I do does not work?
> >
> >    
>
> OK,
>
> But it seems to work !
>
> Ltac bimatch T :=
> match goal with | [h1:T, h2:T |- _] => clear h1 end.
>
>
> Goal nat -> nat -> nat -> nat -> bool.
> intros.
> bimatch nat.
> bimatch nat.
> bimatch nat.
>
> Restart.
>
> intros; repeat bimatch nat.
>
>
> The reason why I proposed another solution was in your first mail:
>
>
>  
>
> > Ltac indom :=
> > match goal with
> > | [h1 : heap; h2 : heap] |- ] => clear h1
> > end.
> > (** doesn't work **)
> >    
>
> In fact, it is syntactically incorrect.
>
> Pierre
>
> If bimatch doesn't fit your requisites, please tell us what the tactic must
> do (i.e. to which kind of goals it must be applied, and which subgoals
> it must generate).
>
>  
Thanks a lot!
By the way, the pattern described in Page 203 of Coq art should be 
corrected, shouldn't it?

Best regards

Sen