New answers tagged


This is not a vim problem, but caused by incorrect building procedure. I refetched the code and build again and this test passed - at the first build I firstly make reconfig then ./configure --disable-gui then make (maybe I did something else I don't remember). I believe the extra make reconfig made something conficted.


Vim syntax is a beast. It takes some time to get used to it. I suggest to try this: scriptencoding utf-8 syn match coqSubscript keepend /\K\d\+/ms=s+1 transparent contains=coqSubscriptDigit \ containedin=ALLBUT,coqComment,coqRequire,coqSubscript,coqSubscriptDigit syn match coqSubscriptDigit /0/ contained conceal cchar=₀ syn match coqSubscriptDigit /1/ ...

Top 50 recent answers are included