diff options
| author | Gaëtan Gilbert | 2019-07-09 12:50:27 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-07-09 12:50:27 +0200 |
| commit | 35d8ca72adcc3ce04cb2919c4a2d60ea0c73d24c (patch) | |
| tree | cd44fa1b1b9e70f73b19d0616499b63016419db9 /vernac | |
| parent | 7f366a7c7cd154c6a1dd191ff7f453e63b39a948 (diff) | |
| parent | dda7d129dba6c90d642cd99cd989e5f13c0eb4b4 (diff) | |
Merge PR #10471: [core] [api] Support OCaml 4.08
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 4 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 2 | ||||
| -rw-r--r-- | vernac/search.ml | 2 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 4 |
4 files changed, 6 insertions, 6 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 90892feb13..e754ead5dd 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -519,7 +519,7 @@ let read_recursive_format sl fmt = let sl = skip_var_in_recursive_format fmt in try split_format_at_ldots [] sl with Exit -> error_not_same ?loc:(fst (List.last (if sl = [] then fmt else sl))) () in let rec get_tail = function - | (loc,a) :: sepfmt, (_,b) :: fmt when Pervasives.(=) a b -> get_tail (sepfmt, fmt) (* FIXME *) + | (loc,a) :: sepfmt, (_,b) :: fmt when (=) a b -> get_tail (sepfmt, fmt) (* FIXME *) | [], tail -> skip_var_in_recursive_format tail | (loc,_) :: _, ([] | (_,UnpTerminal _) :: _)-> error_not_same ?loc () | _, (loc,_)::_ -> error_not_same ?loc () in @@ -953,7 +953,7 @@ let join_auxiliary_recursive_types recvars etyps = | None, None -> typs | Some _, None -> typs | None, Some ytyp -> (x,ytyp)::typs - | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *) + | Some xtyp, Some ytyp when (=) xtyp ytyp -> typs (* FIXME *) | Some xtyp, Some ytyp -> user_err (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++ diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 78112d9dc4..e676fe94db 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -371,7 +371,7 @@ open Pputils | (c,(idl,t))::l -> match factorize l with | (xl,((c', t') as r))::l' - when (c : bool) == c' && Pervasives.(=) t t' -> + when (c : bool) == c' && (=) t t' -> (* FIXME: we need equality on constr_expr *) (idl@xl,r)::l' | l' -> (idl,(c,t))::l' diff --git a/vernac/search.ml b/vernac/search.ml index 101a578587..964d01260b 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -148,7 +148,7 @@ module ConstrPriority = struct -(3*(num_symbols t) + size t) let compare (_,_,_,p1) (_,_,_,p2) = - Pervasives.compare p1 p2 + pervasives_compare p1 p2 end module PriorityQueue = Heap.Functional(ConstrPriority) diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 7644f4c5b6..046defc26b 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -329,8 +329,8 @@ let init_terminal_output ~color = Format.pp_set_print_tags !std_ft true; Format.pp_set_print_tags !err_ft true end; - Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft); - Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft) + Format.pp_set_formatter_tag_functions !std_ft (tag_handler !std_ft) [@warning "-3"]; + Format.pp_set_formatter_tag_functions !err_ft (tag_handler !err_ft) [@warning "-3"] (* Rules for emacs: - Debug/info: emacs_quote_info |