Thanks.  In that case, could you please bisect your local configuration
until you find what causes the issue?



On 27.07.17 15:12, Денис Редозубов wrote:
> I don't think you've missed anything, Charles, it sounds exactly like 
> the way to reproduce it on my machine, the expected behavior would be 
> to see the documentation in a separate buffer.
>
>
> ср, 26 июля 2017 г. в 15:42, Charles A. Roelli <charles@aurox.ch 
> <mailto:charles@aurox.ch>>:
>
>     I have a build environment in macOS Sierra now, so I can try to get it
>     in GDB.
>
>     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 <mailto:rgm@gnu.org>>
>     >> Cc: "Charles A. Roelli" <charles@aurox.ch
>     <mailto:charles@aurox.ch>>, 27761@debbugs.gnu.org
>     <mailto:27761@debbugs.gnu.org>, denis.redozubov@gmail.com
>     <mailto: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
>