coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan Leivent <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Inverse of split tactic?
- Date: Fri, 16 Jan 2015 12:43:12 -0500
On 01/16/2015 12:03 PM, Soegtrop, Michael wrote:
Dear Coq users,
Is there an inverse of the split tactic, that is a tactic that combines the
top two goals into one conjunction goal? This might be handy for
automatically constructing certain terms using Ltac.
Best regards,
Michael
There is no standard tactic to do this. However, I am working on a toolbox of tactics compatible with 8.5 - and one of them combines all focused goals into a single goal - like an inverse of "repeat split". These tactics feature a bunch of "hacks" involving the behavior of evars and tactics-in-terms (the "$(...)$" syntax) in 8.5 that I've been exploring.
-- Jonathan
- [Coq-Club] Inverse of split tactic?, Soegtrop, Michael, 01/16/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
- RE: [Coq-Club] Inverse of split tactic?, Soegtrop, Michael, 01/19/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
- Re: [Coq-Club] Inverse of split tactic?, Jonathan Leivent, 01/16/2015
Archive powered by MHonArc 2.6.18.