The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Fri, Nov 14, 2014 at 07:14:04PM +0000, Colm Bhandal wrote:
> It would be nice if there was a tactic "prune" or something to get rid of
> the duplicate subgoal. Anybody got any ideas how to write a tactic like
> this or does one already exist maybe?

At least in principle it is very easy, a goal is just an evar, and you
can surly unify two evars that have the same associated type and
context.

In trunk goals can be named.  I did not test that, but I guess you can:

  refine ?[theothergoal]. (* or maybe even exact *)

to merge the ongoing goal with another one named "theothergoal".

Best,
-- 
Enrico Tassi