Pierre Courtieu

Right. e-specialize is another problem. Currently `specialize` takes a `constr_with_binding` which binds full constrs, not uconstrs like refine. I don't see a simple way to fix #18332 while still rejecting...

> IIUC we're not talking about specialize per se here, but rather about a derived tactic not present in the Coq distribution. In any case, given your high-level description of...

But I realize that the semantic I am asking needs to be defined clearly. I think the goal I would like to obtain (and would maybe fit into fathomabilty :-)...

And if one wants to have the most general behaviour we should tell which variable should be quantifier existentially. With a reasonable default behaviour.

Here is a complete example of what `especialize H at n` is supposed to do in terms of `refine`. @ppedrot I understand that using `specialize` for that was maybe a...

> both refine and specialize take arguments partially specified terms that may contain holes. By the way what do you mean by that? `specialize` take only plain terms afaik contrary...

Here is my attempt at defining a clean version for the two tactics `specialize` and `especialize`. Both are more verbose that I feel needed in most cases, but at least...

We can then define shortcut versions of `specialize` and `especialize` where the list of premises given by the user is automatically extended with a default strategy before the tactic is...

#18711 shows a use of `specialize` with terms needing (type class) resolution first. I really think `specialize` is like `apply`: it should come in two flavors: one is refine-like, the...

> #18711 shows a use of `specialize` with terms needing (type class) resolution first. I really think `specialize` is like `apply`: it should come in two flavors: one is refine-like,...