Jason Gross

> A question is what kind of object we'd like to return from `Search`, right now we just return names, but certainly a richer information would be appreciated. The amount...

@cpitclaudel do you want me to update this PR with your feedback, or shall we abandon it in favor of https://github.com/ejgallego/coq-serapi/pull/236? (I imagine it'd be easy for you to code...

> Tradeoffs are subtle here tho, a typical example is parsing. Many people have tried to re-implement Coq's parser (with not the best results IMO), where in most cases the...

> You can easily translate between these two, I think, as long as each of the cutoffs is between codepoints. (basically you split the bytestring at positions reported by Coq,...

> > @cpitclaudel do you want me to update this PR with your feedback, or shall we abandon it in favor of [ejgallego/coq-serapi#236](https://github.com/ejgallego/coq-serapi/pull/236)? (I imagine it'd be easy for you...

Note also that mirroring is incompatible with Alectryon's own linking via `alectryon.docutils.COQ_IDENT_DB_URLS`. I agree with @palmskog , when there are any `-Q` or `-R` directives present which capture the given...

Thanks! Is there a way to disable it from my `~/.emacs` (so that when I copy the config to a new machine, I get this automatically)?

Hmmm, well, it doesn't seem to happen with a freshly opened emacs, so something really strange is going on.... (For reference, this is emacs 24.5.1)

This is kind-of important; I'm hitting this natively in Fiat. The timings for ``` coq Time Redirect "/tmp/coq266857Co" Print Ltac Signatures. Time Redirect "/tmp/coq266857Co" Timeout 1 Print Grammar tactic. Time...

> Do you have the `live-on-the-edge` option on? No. Should I turn it on? The relevant bits of my `~/.emacs` are: ``` elisp (defun my-coq-hook () (local-set-key (kbd "C-c RET")...