The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

This is what we've been using:
https://github.com/c-corn/corn/blob/master/tools/coq.mim

On Wed, Mar 2, 2016 at 10:50 AM, Pierre-Marie Pédrot
<pierre-marie.pedrot AT inria.fr>
 wrote:
> On 01/03/2016 12:05, Soegtrop, Michael wrote:
>> If I understand you right, something like this exists for Linux.
>> Could you give a few more pointers?
>
> Yep. The engine I use is ibus:
>
> https://en.wikipedia.org/wiki/Intelligent_Input_Bus
>
> and the particular IME is latex-table, which was originally designed for
> chinese but allows actually to use any input table based on a user-given
> description file (you need to recompile it if you want to change it though).
>
> https://github.com/acevery/ibus-table
>
> https://github.com/acevery/ibus-table/blob/master/tables/additional/latex.txt
>
> I have installed it through Debian, with the ibus-table-latex package.
>
> PMP
>