thirs

This issue seems to have reappeared on my computer: `Compiling file /home/thirs/.emacs.d/elpa/proof-general-20220310.2253/coq/coq-syntax.el at Mon Mar 28 18:04:38 2022 coq-syntax.el:23:1:Error: Cannot open load file: No such file or directory, coq-db `...

Yes, I think I just installed it via melpa, followed the "quick installation instructions" on the website, and tried to open some ".v" file. I then tried with a fresh...

@Matafou It seems to work out of the box on the other computer. ``` thirs ~ $ emacs --version GNU Emacs 27.1 Copyright (C) 2020 Free Software Foundation, Inc. GNU...

@Matafou I forgot to look up the version numbers of the elpa package: on the first machine it was 20220310.2253, while it is 20220328.1209 on the other. So I tried...

Not entirely, but ``` thirs ~ $ locate proof | grep general /home/thirs/.emacs.d/elpa/proof-general-20220328.1209 /home/thirs/.emacs.d/elpa/proof-general-20220328.1209/AUTHORS /home/thirs/.emacs.d/elpa/proof-general-20220328.1209/CHANGES /home/thirs/.emacs.d/elpa/proof-general-20220328.1209/COPYING /home/thirs/.emacs.d/elpa/proof-general-20220328.1209/PG-adapting.info /home/thirs/.emacs.d/elpa/proof-general-20220328.1209/ProofGeneral.info /home/thirs/.emacs.d/elpa/proof-general-20220328.1209/coq ``` seems do say so.

Ok... thanks for your answer. Would you please mind explaining why hoping to use ᵥ instead of _{v} is wrong? It does make latex code much more readable.

Thanks David. How about adding these active characters as an option?

Probably related problem here. Some blocks are displayed as requested, others not. E.g., block Arrows doesn't display with Asana Math as requested. It is probably not an Asana problem though,...

That would be great!

Thanks! But it doesn't appear to change anything. I think it should work to push Asana Math as suggested, but it doesn't. I probably made some stupid configuration mistake. The...