coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Unifying proof goals

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Unifying proof goals
Date: Wed, 1 Aug 2012 20:15:45 -0400

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

[Coq-Club] Unifying proof goals, Jason Gross, 08/02/2012
- Re: [Coq-Club] Unifying proof goals, AUGER Cédric, 08/02/2012