coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?
Date: Mon, 03 Jun 2019 22:27:44 +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:azeYbxSh88/cO7cd+a8QjhmoOdpsv+yvbD5Q0YIujvd0So/mwa68bBKN2/xhgRfzUJnB7Loc0qyK6vmmADdfqs/d7zgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsAndrNQajIVgJ6o+1xfErXlFcPlKyG11Il6egwzy7dqq8p559CRQtfMh98peXqj/Yq81U79WAik4Pm4s/MHkugXNQgWJ5nsHT2UZiQFIDBTf7BH7RZj+rC33vfdg1SaAPM32Sbc0WSm+76puVRTlhjsLOyI//WrKjMF7kaBVrw+7pxFnw4DafpybOvR9cKzTctwVWXFMXtpNWyBdHo+wc5ECA/YHMO1Fr4f9vVwOrR6mCAeuGuzvzCJHhmX33a05zu8vDx/J3QI7H9kTt3nUrMv6NKEPXuCvzanIzi7OYOlN2Tf+8ojHaAotruySUr9pd8fa1EohFxvdg1iTtIDpJS6Z2+UJvmSB8eZsS+Kih3Q6pwx+ojWj3sMhh4nTio8R1lzI7zh1zYY7KNGiRkN2YtipG4ZKuS6ALYt5WMYiTnlouCkkzr0Gvoa2czIRyJQk3R7QceaLfJWW7R77VeaRJyl3hG59db+8mhq+61Wsx+z4W8WuzlpGsCpInsPRun0C1xHf8s2HReF8/kel1zaPzQfT6uRcLEA0i6XbLYMuwqQxlpoQqknMBDT2mEbsjKCMbEkr5/an5/z9Yrr6vp+cK5N0igbmP6syncy/GP00PRQKX2iG4uuxz6bj/E38QLVSlPI6iKjZsJbAJcQavKG1GQFV0pxwoyq4WjyhyZETmWQNBFNDYhOOyYbzaH/UJ/WtLfq5j06tk39Xyu/ddunhD5PBNHnAuL76fqx0rUJRnllghetD7o5ZX+lSaMn4XVX84YSBX00JdjesyuOiM+1Tk4YXWGaBGKicafuAuESL/OtpL+TePNZI6ga4EOAs4rvVtVF8mVIZevDxj5IMa2qxWPhrcR3APSjcx+wZGGJPhTIQCfTwgQTaAzdIZGy7Ga4xtGk2

Hi,

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?

Background: I trying to reactivate prooftree, the interactive
proof tree display support for Proof General. Prooftree
asynchronously sends Show Goal commands to Coq to receive the
full text for new subgoals or, after instantiating existentials,
the updated goal text. The goal id's do still exist, even in Coq
8.9. You can see them with coq -emacs (or in Proof General).

Thanks,

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