search

VSpaceCode / vspacecode.github.io

VSpaceCode website
https://vspacecode.github.io
3 stars 23 forks source link

Add coq major mode docs #56

Closed ayanamists closed 2 years ago

ayanamists commented 2 years ago

Add docs with marketplace link.

stevenguh commented 2 years ago

Thanks. Do you think it would be helpful to list the known issue you mentioned in https://github.com/VSpaceCode/VSpaceCode/pull/253

Known Problems:

  • proof-goto-point will goto the previous tactic when cursor is at the . symbol. This is caused by extension.coq.interpretToPoint command of vscoq
ayanamists commented 2 years ago

Thanks. Do you think it would be helpful to list the known issue you mentioned in VSpaceCode/VSpaceCode#253

Known Problems:

  • proof-goto-point will goto the previous tactic when cursor is at the . symbol. This is caused by extension.coq.interpretToPoint command of vscoq

I think it need not to be mentioned because it will be the same when user in vim normal mode and press alt + →(the default shoutcut of extension.coq.interpretToPoint)

stevenguh commented 2 years ago

Sounds good. Merged :) Thanks