diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 2 | ||||
| -rw-r--r-- | ide/texmacspp.ml | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index bb8723dfe6..5b07d3ec3b 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -100,7 +100,7 @@ let coqide_cmd_checks (loc,ast) = if is_debug ast then user_error "Debug mode not available within CoqIDE"; if is_known_option ast then - Feedback.msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + Feedback.msg_warning (strbrk"This will not work. Use CoqIDE view menu instead"); if Vernac.is_navigation_vernac ast || is_undo ast then Feedback.msg_warning (strbrk "Rather use CoqIDE navigation instead"); if is_query ast then diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 53a29008ad..680da7f54b 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -189,7 +189,8 @@ match sm with end | SetEntryType (s, _) -> ["entrytype", s] | SetOnlyPrinting -> ["onlyprinting", ""] - | SetOnlyParsing v -> ["compat", Flags.pr_version v] + | SetOnlyParsing -> ["onlyparsing", ""] + | SetCompatVersion v -> ["compat", Flags.pr_version v] | SetFormat (system, (loc, s)) -> let start, stop = unlock loc in ["format-"^system, s; "begin", start; "end", stop] @@ -708,6 +709,7 @@ let rec tmpp v loc = | VernacSetStrategy _ as x -> xmlTODO loc x | VernacUnsetOption _ as x -> xmlTODO loc x | VernacSetOption _ as x -> xmlTODO loc x + | VernacSetAppendOption _ as x -> xmlTODO loc x | VernacAddOption _ as x -> xmlTODO loc x | VernacRemoveOption _ as x -> xmlTODO loc x | VernacMemOption _ as x -> xmlTODO loc x |