coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?

From: Hendrik Tews <hendrik AT askra.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?
Date: Wed, 05 Jun 2019 23:32:24 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=hendrik AT askra.de; spf=None smtp.mailfrom=hendrik AT askra.de; spf=None smtp.helo=postmaster AT askra.de
Ironport-phdr: 9a23:EdjUYh9XLSP5hf9uRHKM819IXTAuvvDOBiVQ1KB40eIcTK2v8tzYMVDF4r011RmVBNydsq4ewLOI6OjJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVmTaxe65+IRqooQneq8UbgIVvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFojKxVvg+vqB5xw4Habo+bN/Vxcb/GcNMGWWZNQtpdWzBbD4+gaYYEEuoPPfxfr4n4v1YArwWxBQ+xC+P1yz9IhWL907Mk3OUvCgHNwQstH9IQv3TSsdr1LqYSUeOuwabS1jXDbOlW1i3n5IfVbB8suPeBVq9+f8rWzEkgDQLFjlOIpIzqPjOVyuQNs3WA4OZ6Se2vjGsnpgdsqTas3schkorEip8PxlzZ9Ch0xJw5KcOmREN7e9KoDZRduiGCO4ZyQs4uWWVltDogxrEbuZO2cjIGxZokyhPZdveJaZKH4gj5W+aUOTp4hGxqeLa4hxuq60eg0e78VtOu31pQsyVKjMHAtnEL1xPN9siKUvhw8lq71TqS1g3e7vtILV4qmafbMZIt37E9m5oLvUTGBCD2mUH2jKGMdkUj/+il8+TnbavgppCBLY90iwL+P780lcykAuQ4KBIBU3KG9uuizLHj51H2QK1Wjv0qlanUqIzVJcMCpqKgHwBV1psj5A2kAje90NUYmGEHI0hfdBKGiYjpIVDOL+riAfexmVT/2AtskvvBJ/jqBojHBnnFirboO7hnuGBGzw9m7d1Z64hVCfk9Le3oEhvxudrUFB46GwWvwPzuTtlwgNBNEVmTC7OUZfuB+WSD4fgidrHVON0l/Q3lIv1g3MbAyGcjkAZFL6Cy3oEeLny1TKw/fhepJEH0i9JEKl8k+wozSOuz0A+LSj1JbjC+UvBkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkeWFmXEm3hMYmJCa8B

Jim Fehrle
<jim.fehrle AT gmail.com>
writes:

> you open an issue for this in GitHub and send me the link? That

See https://github.com/coq/coq/issues/10315

> First questions to answer in the issue: You want to use goal

I tried to answer that with a different example, because I wanted
to show existential variables and because I could not find
test.3.v.

Best regards,

Hendrik

[Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?, Hendrik Tews, 06/03/2019
- Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?, Emilio Jesús Gallego Arias, 06/03/2019
  - Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?, Hendrik Tews, 06/04/2019
    - Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?, Jim Fehrle, 06/05/2019
      - Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?, Hendrik Tews, 06/05/2019
    - Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?, Emilio Jesús Gallego Arias, 06/05/2019