The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/15/2014 04:06 AM, Enrico Tassi wrote:
> 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,

Yes - this works in the trunk:

Variable P : Prop.
Axiom okP : P.

Goal P /\ P.
split.
Show Existentials. (*shows ?Goal0 and ?Goal1 as the goal names*)
exact ?Goal1.
apply okP.
Qed.

However, there currently is no cyclicity check, as this:

Goal False.
exact ?Goal.
Qed.

just loops forever at Qed.