You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In the spirit of merlin, and other interactive theorem provers, it would be nice to map \leader<letter> to some useful commands. For instance, when the cursor is on a symbol, \leader p could call :Coq Print <symbol> to print the value, and \leader t could call :Coq Check <symbol>.
A shortcut for SearchAbout would be awesome, too. And syntax coloring in Infos/Goals windows!
The text was updated successfully, but these errors were encountered:
About the syntax coloring in Infos/Goals windows, could you give a try to my fork https://github.com/lgeorget/coquille? Please report bugs. Once I have enough feedback and my coloring is ok, I'll send a pull request here.
In the spirit of merlin, and other interactive theorem provers, it would be nice to map
\leader<letter>
to some useful commands. For instance, when the cursor is on a symbol,\leader p
could call:Coq Print <symbol>
to print the value, and\leader t
could call:Coq Check <symbol>
.A shortcut for SearchAbout would be awesome, too. And syntax coloring in Infos/Goals windows!
The text was updated successfully, but these errors were encountered: