The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/11/2016 05:35 AM, Pierre Courtieu wrote:
> Nice, thanks Jonathan!
>
> One small glitch yet: the name of the re-asbtracted hypothesis are not kept
> the same. I guess it is hard to keep them around.
>
> P.
Unfortunately, I don't think there's a way to keep the names and also 
get the generality and fairly nice syntax, because of limitations of 
Ltac.   For instance, if you are willing to limit the args to those 
specifying numeric positions of non-dependent parameters - like the "(2 
:= H0)" in your example - then it might be possible, especially if you 
limit it to one such arg per call.

However, even though Ltac can do some interesting things here, I think 
it would be better if a built-in tactic provided this behavior.  On 
coqdev, there have been some discussions of what people would like the 
refine tactic to do in terms of specifying which arguments are shelved 
vs. not, and adding which should be left abstracted to that seems natural.

-- Jonathan