|
From: | Charles A. Roelli |
Subject: | bug#27761: Crash while using proof-general/company-coq on OS X |
Date: | Wed, 26 Jul 2017 21:42:30 +0200 |
Denis: I have the requirements for the file installed (Metalib, Stlc).I go to line 166 in Stlc/Lemmas.v, type C-c C-RET, type 'intuition', to get this:
pose proof size_typ_min_mutual as H; intuition eauto.intuition And then hit C-h. I get no crash (no documentation popup shows either, though). Did I miss a step? On 24.07.17 19:02, Eli Zaretskii wrote:
From: Glenn Morris <rgm@gnu.org> Cc: "Charles A. Roelli" <charles@aurox.ch>, 27761@debbugs.gnu.org, denis.redozubov@gmail.com Date: Mon, 24 Jul 2017 12:58:49 -0400 Is it impossible to "provide a minimal example starting from emacs -Q" for this issue?I still hope it will be possible. Alternatively, if someone catches this in GDB, I can ask a few questions and probably understand what's going on, the reason cannot be too complicated. TIA
[Prev in Thread] | Current Thread | [Next in Thread] |