The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Jean.Duprat wrote:

> Hi,
>
> What is the role of "ipattern:" which is largely used by the 
> translator V7 -> V8 and
> that V8.0beta dislikes ?

the ipattern: construct allows to pass an intro-pattern (the argument of 
the intros tactic) to a Ltac.
Normally, the arguments of Ltacs sould be terms. It is similar to ltac: 
which is used to pass an argument that is
the result of an Ltac expression. Assume we wanted to defined an Ltac 
that introduces new hypotheses which name
is passed as arguments (not passing names and letting the tactic choose 
names is considered a bad style, even if many standard
tactics do it), for instance

Ltac my_intro H1 H2 := intros H1 H2.
(OK it's dumb to define that tactic, but it's just to avoid unnecessary 
details).

Without ipattern, you would not be able to use my_intro.
If you type my_intro h0 h1, then either h0 and h1 do not exist and the 
globalization of the arguments fail, or they already exist, and then the 
intros fail.
Instead, you can do my_intro ipattern:h0 ipattern:h1 which will do what 
expected.
I recognize the syntax is not as lightweight as one could expect, but we 
had to make a trade-off. Globalization helps finding mis-spelled 
arguments, and we definitely want to avoid too cryptic notations such as 
ipatt: , ipat: or ip: ...

Bruno Barras.