Consistency with proof general?

[cpitclaudel]

Hey @kyoDralliam,,

Have you seen the recently merged Coq layer? Maybe it would make sense to unify the keybindings that do roughly the same thing?

Also, should there be a link to this repo in the fstar-mode readme?

[kkohbrok]

A link to the spacemacs layer would have been useful, at least for me. I only just found this and had previously used fstar-mode without a layer.

[kyoDralliam]

Hi @cpitclaudel,
I didn't know about this coq layer, I will have a look at it and see how I can integrate things in this layer.

Otherwise, the status of this repo is still rather experimental. If I have enough time I will try to complete this layer wrt to your fstar-mode and try to merge it officially once it is ready.

[cpitclaudel]

Thanks! Feel free to add a link to it from fstar-mode's README when you feel it's ready.

[theolaurent]

Digging up the issue, I think it would make sense to make this layer closer to the coq layer in terms of key bindings (as I am using both). And am willing to make it happen, but it obviously is quite a change for the user. So @cpitclaudel do you still think it should be done?

[cpitclaudel]

@theolaurent I don't use either layers, as I don't use spacemacs. I just had people mention the inconsistency to me and so created an issue.