diff --git a/src/plugins/e-acsl/src/analyses/interval.ml b/src/plugins/e-acsl/src/analyses/interval.ml
index 86bcf2fb9a0eeb50b2baca1349ac9b18d3739451..ac50f02b6a22508937636a8726ed92288edc9aa3 100644
--- a/src/plugins/e-acsl/src/analyses/interval.ml
+++ b/src/plugins/e-acsl/src/analyses/interval.ml
@@ -400,7 +400,6 @@ module Profile = struct
       (struct
         let module_name = "E_ACSL.Interval.Logic_function_env.Profile"
       end)
-  let is_included p1 p2 = List.for_all2 is_included p1 p2
 end
 
 (* Imperative environments *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index d4022ccc0b1b038eddc2b4324531bbb5bda60532..6394220aca7985b7086fe0bf61c0887b4acf082a 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -199,8 +199,7 @@ module Memo: sig
     (term -> computed_info) ->
     term ->
     computed_info Error.result
-  val get: lenv:Function_params_ty.t -> term ->
-    computed_info Error.result
+  val get: lenv:Function_params_ty.t -> term -> computed_info Error.result
   val clear: unit -> unit
 end = struct
 
diff --git a/src/plugins/e-acsl/src/libraries/error.ml b/src/plugins/e-acsl/src/libraries/error.ml
index 1b32febdce7a0fec8334dbcd7246080599f18543..4e23a5700617c12c04c759a50299d4b4a17b115f 100644
--- a/src/plugins/e-acsl/src/libraries/error.ml
+++ b/src/plugins/e-acsl/src/libraries/error.ml
@@ -54,6 +54,9 @@ module type S = sig
     Format.formatter ->
     'a result ->
     unit
+  val map: ('a -> 'b) -> 'a result -> 'b
+  val map2: ('a -> 'b -> 'c) -> 'a result -> 'b result -> 'c
+  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a result -> 'b result -> 'c result -> 'd
 end
 
 module Make_with_opt(P: sig val phase:Options.category option end): S = struct
@@ -125,6 +128,24 @@ module Make_with_opt(P: sig val phase:Options.category option end): S = struct
     match res with
     | Result.Ok a -> Format.fprintf fmt "@[%a@]" pp a
     | Result.Error err -> Format.fprintf fmt "@[%s@]" (Printexc.to_string err)
+
+  let map f = function
+    | Result.Ok a -> f a
+    | Result.Error e -> raise e
+
+  let map2 f a b =
+    match a,b with
+    | Result.Ok a, Result.Ok b -> f a b
+    | Result.Ok _, Result.Error e -> raise e
+    | Result.Error e, _ -> raise e
+
+  let map3 f a b c =
+    match a,b,c with
+    | Result.Ok a, Result.Ok b, Result.Ok c -> f a b c
+    | Result.Ok _, Result.Ok _, Result.Error e -> raise e
+    | Result.Ok _, Result.Error e, _ -> raise e
+    | Result.Error e, _, _ -> raise e
+
 end
 
 module Make(P: sig val phase:Options.category end): S =
diff --git a/src/plugins/e-acsl/src/libraries/error.mli b/src/plugins/e-acsl/src/libraries/error.mli
index 599ec5cd1bb75d6f3c6d4d5c5ce1307d45e9577a..a4a690ab56a1d450b0993c1e4806a9f743056021 100644
--- a/src/plugins/e-acsl/src/libraries/error.mli
+++ b/src/plugins/e-acsl/src/libraries/error.mli
@@ -81,8 +81,14 @@ module type S = sig
     Format.formatter ->
     'a result ->
     unit
-    (** [pp_result pp] where [pp] is a formatter for ['a] returns a formatter for
-        ['a result]. *)
+  (** [pp_result pp] where [pp] is a formatter for ['a] returns a formatter for
+      ['a result]. *)
+
+  val map : ('a -> 'b) -> 'a result -> 'b
+  val map2 : ('a -> 'b -> 'c) -> 'a result -> 'b result -> 'c
+  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a result -> 'b result -> 'c result -> 'd
+  (** Apply a function to one or several results and propagate the errors *)
+
 end
 
 (** Functor to build an [Error] module for a given [phase]. *)