The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

The method of agda is implemented via emacs input methods, it is also
possible to use this method in proofgeneral and any other emacs mode:

simply type:
M-x set-input-method <return> TeX <return>

for coqide the only method I know of is the one explained in the coq
reference manual:

http://coq.inria.fr/coq/refman/Reference-Manual019.html#toc106

Hope this helps,
Pierre Courtieu



2010/2/17 Bas Spitters 
<spitters AT cs.ru.nl>:
> What method do people use to input unicode characters, preferably
> methods that work with coqide.
>
> The agda way seems nice:
> http://wiki.portal.chalmers.se/agda/agda.php?n=Docs.UnicodeInput
>
> Thanks,
>
> Bas
>