Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Inverse of split tactic?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Inverse of split tactic?


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page