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: Emilio Jesús Gallego Arias <e AT x80.org>
To: Hendrik Tews <hendrik AT askra.de>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?
Date: Mon, 03 Jun 2019 23:04:53 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:6Er6TBLVliSdXPbQVNmcpTZWNBhigK39O0sv0rFitYgRI/7xwZ3uMQTl6Ol3ixeRBMOHsqsC0rGJ+Pm9AiQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfL9+Ngi6oAvTu8UZnIdvKqg8wQbVr3VVfOhb2XlmLk+JkRbm4cew8p9j8yBOtP8k6sVNT6b0cbkmQLJBFDgpPHw768PttRnYUAuA/WAcXXkMkhpJGAfK8hf3VYrsvyTgt+p93C6aPdDqTb0xRD+v4btnRAPuhSwaLDMy7n3ZhdJsg6JauBKhpgJww4jIYIGOKfFyerrRcc4GSWZdW8pcUTFKDIGhYIsVF+cPPfhWoZT6p1sAoxWxBwqiC+3gxTBUnXL2wbE23v49HQ3axgEtHdQDu2nUotXvM6cSVPi4wqbNzTXCa/NW2DD955DMfB8/uvGUR6lwftLQx0Y1EwPFikufqYPiPzyNyukNqWmb4PB7VemyjGMotRp8ozesy8swkIXJgZgVyl/d+Ch/3Y07K9q4SEthbt6lFptdry6aN4pqQsMiXmFnozw2xaEBuZ6+eiUB1ZcpxwbHZvCacIWF4QjvWPiPLTp5nn5pZbCyiwuo/US9xODwSNG43VVLoyZfk9TBtGoB2hjJ5sSaRPZw8EGs0iuV2Q/J8OFLO0U0mLLbK5E/xr4wkYIesEvAEyPqgkn2i7WWdko89uip7eTofKnmq4eBO4J3iQzyKLoiltK+DOgiLwQDXXWX9f6h2LDt40H1WLBKgec3kqndvpDaP8MbpquhDgBLyYsi5BWyAyu83NQfh3kHI0pJeAibgIjxJ1HOPPf4AO+jjFSriTdn3uzJPrn8AprWNXXDi7fgfbNl60FG0gYzzNZf54hVCr4bOv7zVFXx55TkCUoZPgq42efkQOlwyZhWDWKCBKODMaD6uESL/OtpL+TaN6EPvzOoBv0k4//pul00gs0GSoag2Z8aZ3ePN+5nKl7RNXfEkodZV2AQsVxtH6TRlFSeXGsLND6JVKUm62R+Udr+VNaRdsWWmLWEmRyDMNhTb2FCBEqLFCa6Z9XcHfAWZ3DLe5Izonk/TbGkDrQZ+1SuuQv9muh3frKS/TcX58u6iIpFotbLnBR3zgRaStyH2jDfXzEs2GQSSG1u0Q==
Organization: X80 Heavy Industries

Hi Hendrik,

Hendrik Tews
<hendrik AT askra.de>
writes:

> in Coq 8.6 one could, for instance, use ``Show Goal "6".'' to
> print the goal with the unique, non-changing identifier 6. For
> instance after
>
> Lemma l : forall(P : Prop), P -> P /\ P.
> Proof using.
> intros P H.
> split.
>
> the command
>
> Show Goal "6".
>
> prints the second subgoal. In Coq 8.7.0 or later Show Goal with
> quotation marks does not work any more. Could somebody tell me
> the new syntax?

I'm not sure there's a new syntax, see the removal PR
https://github.com/coq/coq/pull/765

I guess that command could be re-instantiated, or you could use Goal
identifiers, however, I am not sure if using the toplevel protocol to
implement proof tree display will be robust enough as to survive for
long.

Best regards,
E.

[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