The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Wed, 1 Aug 2012 20:15:45 -0400,
Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> Hi,
> If I have two proof goals that are identical, is there a way to tell
> Coq "get rid of one of the proof goals because it's the same as this
> one"?  Or something (a variant of [abstract], maybe?) that says
> "solve these both using this tactic, but only run the tactic once,
> because it's expensive"?
> 
> Thanks.
> 
> -Jason

I guess it is not what you want, but you still can use
cut/assert/pose/set tactics. You can even use a "refine (let H :
<your proof> := _ in _)." or variants if you want to be at a very low
level.

Of course that needs to identify the goals you will need to unify
before trying to solve them.