The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Hey,

There is a difference between [intro] and [intros] when they don't have a parameter: [intro] introduces the first product, even if it needs to head-reduce the goal to make it appear, [intros] introduces all the visible products. These are, incidentally the behaviour of [intros ?] and [intros **] respectively. As I really consider it ill-advised to use the argument-free version, I agree with you that the difference is mostly artificial and could probably be easily fixed. Maybe you should make a feature wish on coq-bugs so that it can be discussed there: I have time to do it, but I don't wish to take this decision without some amount of discussion (and the next release is now very close).

The actual reason for the dichotomy is, of course, history. Generally speaking there is a significant amount of work to go through the basic tactics and sort out what the main set should be. Maybe [intro] can make it into v8.5 though.

On 13 December 2014 at 14:00, Frederic Chyzak <frederic.chyzak AT inria.fr> wrote:

Hi,

I'm a newbie who has just taken his first lesson of (plain) Coq, now
trying his very first (plain) Coq exercises.

Many times, I find myself starting with some "intro x.", before
realizing I need to introduce another hypothesis, thus typing " y".
But, then, "intro x y." is an error, and I need to add an "s", to write
"intros x y.".

Is there a use case that motivates having two different tactic names?
Why not just make them absolute synonyms?

The problem is that I would like to use the same name, irrespective of
the number of arguments, and for that I would prefer typing the shorter
"intro".

Frédéric