coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] goal selectors; tactic expressions

From: David Holland <dholland-coq AT netbsd.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] goal selectors; tactic expressions
Date: Thu, 24 Jan 2019 18:06:12 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=dholland-coq AT netbsd.org; spf=Pass smtp.mailfrom=dholland AT netbsd.org; spf=None smtp.helo=postmaster AT mail.netbsd.org
Ironport-phdr: 9a23:nXEKgBNDESYRnhaPn3El6mtUPXoX/o7sNwtQ0KIMzox0LPXyrarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSkJNzA37nzZhM9+jK1UvB2uuh5wzIDPbYGJKPZzZL/Rcc8ASGZfWMtaSixPApm7b4sKF+cPM/xXr5f8p1QTsBCwBw6sBOfryjBSgH/5wLAx3uM8HgHG2wwgG9YOv27SrNroLasdTee1zLDTwDXFcfxWxSzy6JPVfRw7pvGMR71wfNPXxEIyFA3Flk2dpZHhMj6RzOgBrWaW4uR6We6xlmIqqRt9riazysswjITCm5gbxUre9SpjxYY4Pd24R1B/Yd6jCJZQsjuVN4pyQs84RWFnpjo6xaYduZGmZiQKz44nxxHHZ/yGdYiH/A7jWf6MLTp8gH9pYqyzihi8/ES61OHwS8u53ExUoiZZjtXArnUN2AbS6siDRPt95ECh2TOX2g/O6uFEJkQ0la7BJJ4n37E9jZwTvlrfHiDtg0X5kbWadkI++uin8+jneKnppoeAN49ojQHzKrghmsumAeghLgcOW3Wb9v+n2b34/Uz5Ra1KgecsnqnYtpDaP8UbqbSjDw9byIZwoyq4WjyhyZETmWQNBFNDYhOOyYbzaH/UJ/WtIf6hgljksDBvw/nAMvW1DpXKKnzKlrukdrFkw0hR1AAowZZY/Z0CWeJJG+76RkKk7I+QNRQ+KQHhm7+2WuU47ZsXXCe0OoHcNarTtVGS4ed2ebuKaZMfozq7LOIqtae30S0J3GQFdKzs5qM5LWiiF608cUOUfXD3jpEGC2hY5lNjHtyvs0WLVHtoX1j3X6844WhkWoevDIOFQI2xiqeNmiChEc8Oaw==

On Thu, Jan 24, 2019 at 01:05:38PM +0100, Laurent Thery wrote:
> On 1/24/19 5:35 AM, Jeremy Dawson wrote:
> > ow do I write a tactic to repeatedly apply solve_eqs to goals 1 and 2
> > until either both are solved or there is no further progress?
>
> Maybe you are mislead by the fact that the goal numbering is local but
> not global

Furthermore, nontrivial operations often reorder the goal list, so
what you're trying to do may not work anyway :-(

--
David A. Holland
dholland AT netbsd.org

[Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/24/2019
- Re: [Coq-Club] goal selectors; tactic expressions, Laurent Thery, 01/24/2019
  - Re: [Coq-Club] goal selectors; tactic expressions, David Holland, 01/24/2019
  - Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/24/2019
    - Re: [Coq-Club] goal selectors; tactic expressions, Cyprien Mangin, 01/25/2019
      - Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
        
        Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
        
        Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
        
        Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
        Re: [Coq-Club] goal selectors; tactic expressions, Jeremy Dawson, 01/25/2019
        Re: [Coq-Club] goal selectors; tactic expressions, Jason -Zhong Sheng- Hu, 01/25/2019
        Re: [Coq-Club] goal selectors; tactic expressions, Gaëtan Gilbert, 01/25/2019
        Re: [Coq-Club] goal selectors; tactic expressions, Théo Zimmermann, 01/25/2019