The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

I'm findind the with extension for writing tactics very useful. 

For example

Repeat Rewrite My_theorem with a := a

instantiate my theorem so to restrict the possible rewriting

Apply My_theorem with 1:= H

instantiante first a theorem with the local context before applying
it.

I'm wondering why this is not allowed for all tactics?

For example

Generalize My_theorem with 1:= H.

would shorten the ugly Generalize [x,y,z:?] (My_theorem x y z H).

As a matter of fact, the best would be that the with extension
would be considered not a the tactic level but at the term level.

So 

   Apply My_theorem with 1:= H.

would mean 

  Apply (My_theorem with 1:= H).

and in particular 

  (My_theorem with 1:= H) 

would be a licite term. This would have the advantage to make
the with extension available for homemade tactics.


--
Laurent Thery