Merge branch 'trunk' into located_switch

9 files changed, 42 insertions, 25 deletions

diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index fe6e87388..09a254e9d 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -58,7 +58,7 @@ let record_in_aux_at ?loc key v =
 
 let current_loc : Loc.t option ref = ref None
 
-let record_in_aux_set_at ?loc = current_loc := loc
+let record_in_aux_set_at ?loc () = current_loc := loc
 
 let record_in_aux key v = record_in_aux_at ?loc:!current_loc key v
 
diff --git a/lib/aux_file.mli b/lib/aux_file.mli
index 41b7b0855..a7960fa16 100644
--- a/lib/aux_file.mli
+++ b/lib/aux_file.mli
@@ -24,4 +24,4 @@ val recording : unit -> bool
 
 val record_in_aux_at : ?loc:Loc.t -> string -> string -> unit
 val record_in_aux : string -> string -> unit
-val record_in_aux_set_at : ?loc:Loc.t -> unit
+val record_in_aux_set_at : ?loc:Loc.t -> unit -> unit
diff --git a/lib/backtrace.ml b/lib/backtrace.ml
index b3b8bdea2..be9f40c1f 100644
--- a/lib/backtrace.ml
+++ b/lib/backtrace.ml
@@ -5,6 +5,7 @@
 (*    //   *      This file is distributed under the terms of the      *)
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
+[@@@ocaml.warning "-37"]
 
 type raw_frame =
 | Known_location of bool   (* is_raise *)
diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index 1c1ff7e2f..b55fd80c6 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -121,12 +121,14 @@ end
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user. *)
 
+[@@@ocaml.warning "-52"]
 let noncritical = function
   | Sys.Break | Out_of_memory | Stack_overflow
   | Assert_failure _ | Match_failure _ | Anomaly _
   | Timeout | Drop | Quit -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
+[@@@ocaml.warning "+52"]
 
 (** Check whether an exception is handled *)
 
diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml
index ececc6308..2755946ab 100644
--- a/lib/cWarnings.ml
+++ b/lib/cWarnings.ml
@@ -75,7 +75,7 @@ let set_all_warnings_status status =
 
 let set_category_status ~name status =
   let names = Hashtbl.find categories name in
-  List.iter (fun name -> set_warning_status name status) names
+  List.iter (fun name -> set_warning_status ~name status) names
 
 let is_all_keyword name = CString.equal name "all"
 let is_none_keyword s = CString.equal s "none"
@@ -159,7 +159,7 @@ let normalize_flags_string s =
     let flags = normalize_flags ~silent:false flags in
     string_of_flags flags
 
-let rec parse_warnings items =
+let parse_warnings items =
   CList.iter (fun (status, name) -> set_status ~name status) items
 
 (* For compatibility, we accept "none" *)
diff --git a/lib/feedback.ml b/lib/feedback.ml
index 3552fa4a0..f6abf6512 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -40,8 +40,6 @@ type feedback = {
   contents : feedback_content;
 }
 
-let default_route = 0
-
 (** Feeders *)
 let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7
 
diff --git a/lib/option.ml b/lib/option.ml
index fbb883d30..50fdd079d 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -20,24 +20,24 @@ let has_some = function
   | _ -> true
 
 let is_empty = function
-| None -> true
-| Some _ -> false
+  | None -> true
+  | Some _ -> false
 
 (** Lifting equality onto option types. *)
 let equal f x y = match x, y with
-| None, None -> true
-| Some x, Some y -> f x y
-| _, _ -> false
+  | None, None -> true
+  | Some x, Some y -> f x y
+  | _, _ -> false
 
 let compare f x y = match x, y with
-| None, None -> 0
-| Some x, Some y -> f x y
-| None, Some _ -> -1
-| Some _, None -> 1
+  | None, None -> 0
+  | Some x, Some y -> f x y
+  | None, Some _ -> -1
+  | Some _, None -> 1
 
 let hash f = function
-| None -> 0
-| Some x -> f x
+  | None -> 0
+  | Some x -> f x
 
 exception IsNone
 
@@ -57,13 +57,11 @@ let init b x =
   else
     None
 
-
 (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 let flatten = function
   | Some (Some y) -> Some y
   | _ -> None
 
-
 (** [append x y] is the first element of the concatenation of [x] and
     [y] seen as lists. *)
 let append o1 o2 =
@@ -134,6 +132,7 @@ let cata f a = function
   | Some c -> f c
   | None -> a
 
+
 (** {6 More Specific operations} ***)
 
 (** [default a x] is [y] if [x] is [Some y] and [a] otherwise. *)
@@ -165,7 +164,6 @@ let lift2 f x y =
   | _,_ -> None
 
 
-
 (** {6 Operations with Lists} *)
 
 module List =
@@ -183,9 +181,19 @@ module List =
     | [] -> []
 
   let rec find f = function
-    |[] -> None
-    |h :: t -> match f h with
-	 |None -> find f t
-	 |x -> x
+    | [] -> None
+    | h :: t -> match f h with
+	 | None -> find f t
+	 | x -> x
+
+  let map f l =
+    let rec aux f l = match l with
+    | [] -> []
+    | x :: l ->
+      match f x with
+      | None -> raise Exit
+      | Some y -> y :: aux f l
+    in
+    try Some (aux f l) with Exit -> None
 
 end
diff --git a/lib/option.mli b/lib/option.mli
index 5e085620e..f06ad9f1d 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -122,5 +122,14 @@ module List : sig
       [Some y] (in the same order). *)
   val flatten : 'a option list -> 'a list
 
+  (** [List.find f l] is the first [f a] different from [None],
+      scrolling through elements [a] of [l] in left-to-right order;
+      it is [None] if no such element exists. *)
   val find : ('a -> 'b option) -> 'a list -> 'b option
+
+  (** [List.map f [a1;...;an]] is the list [Some [b1;...;bn]] if
+      for all i, there is a [bi] such that [f ai] is [Some bi]; it is
+      [None] if, for at least one i, [f ai] is [None]. *)
+  val map : ('a -> 'b option) -> 'a list -> 'b list option
+
 end
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 34d49685b..29f020071 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -32,7 +32,6 @@ let compare = Int.compare
 module Self = struct
  type t = int
  let compare = compare
- let equal = equal
 end
 
 module Set = Set.Make(Self)