aboutsummaryrefslogtreecommitdiff
path: root/ide/coqide/protocol
AgeCommit message (Collapse)Author
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
2020-10-08Add a check of empty list of arguments in xmlprotocol where relevant.Hugo Herbelin
2020-06-02Move CoqIDE to its own folderMaxime Dénès
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.