diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/protocol/richpp.ml | 6 | ||||
| -rw-r--r-- | ide/session.ml | 4 | ||||
| -rw-r--r-- | ide/wg_Completion.ml | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/ide/protocol/richpp.ml b/ide/protocol/richpp.ml index 507b985d2f..463d93af0d 100644 --- a/ide/protocol/richpp.ml +++ b/ide/protocol/richpp.ml @@ -94,7 +94,7 @@ let rich_pp width ppcmds = print_close_tag = ignore; } in - pp_set_formatter_tag_functions ft tag_functions; + pp_set_formatter_tag_functions ft tag_functions [@warning "-3"]; pp_set_mark_tags ft true; (* Setting the formatter *) @@ -107,9 +107,9 @@ let rich_pp width ppcmds = (* The whole output must be a valid document. To that end, we nest the document inside <pp> tags. *) pp_open_box ft 0; - pp_open_tag ft "pp"; + pp_open_tag ft "pp" [@warning "-3"]; Pp.(pp_with ft ppcmds); - pp_close_tag ft (); + pp_close_tag ft () [@warning "-3"]; pp_close_box ft (); (* Get the resulting XML tree. *) diff --git a/ide/session.ml b/ide/session.ml index 3792730455..a9c106a765 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -275,9 +275,9 @@ let make_table_widget ?sort cd cb = let make_sorting i (_, c) = let sort (store : GTree.model) it1 it2 = match c with | `IntC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) | `StringC c -> - Pervasives.compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) + compare (store#get ~row:it1 ~column:c) (store#get ~row:it2 ~column:c) in store#set_sort_func i sort in diff --git a/ide/wg_Completion.ml b/ide/wg_Completion.ml index 7758d89ed8..98390e810f 100644 --- a/ide/wg_Completion.ml +++ b/ide/wg_Completion.ml @@ -15,7 +15,7 @@ struct (* we use first size, then usual comparison *) let d = String.length s1 - String.length s2 in if d <> 0 then d - else Pervasives.compare s1 s2 + else compare s1 s2 end module Proposals = Set.Make(StringOrd) |