coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- 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/04/2019
- Re: [Coq-Club] Show Goal "<goal-id>" in Coq 8.7 or later?, Emilio Jesús Gallego Arias, 06/03/2019
Archive powered by MHonArc 2.6.18.