Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


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



Archive powered by MHonArc 2.6.18.

Top of Page