diff --git a/src/plugins/e-acsl/src/analyses/lscope.ml b/src/plugins/e-acsl/src/analyses/lscope.ml
index ccf0726b033dfa66f046a0593117e3f4de5f6525..56a9e7ff0fd4d13e4598f15b369e0333686ea6bd 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.ml
+++ b/src/plugins/e-acsl/src/analyses/lscope.ml
@@ -47,6 +47,8 @@ let exists lv t =
   in
   List.exists is_lv t
 
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+
 exception Lscope_used
 let is_used lscope pot =
   let o = object inherit Visitor.frama_c_inplace
@@ -57,8 +59,14 @@ let is_used lscope pot =
   in
   try
     (match pot with
-     | Misc.PoT_pred p -> ignore (Visitor.visitFramacPredicate o p)
-     | Misc.PoT_term t -> ignore (Visitor.visitFramacTerm o t));
+     | PoT_pred p -> ignore (Visitor.visitFramacPredicate o p)
+     | PoT_term t -> ignore (Visitor.visitFramacTerm o t));
     false
   with Lscope_used ->
     true
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/analyses/lscope.mli b/src/plugins/e-acsl/src/analyses/lscope.mli
index f84968eeaa3926b0ca8cefff034d58659b81fc1b..56728c2bdd002181bb5c4a62743ab6cfaac7afd9 100644
--- a/src/plugins/e-acsl/src/analyses/lscope.mli
+++ b/src/plugins/e-acsl/src/analyses/lscope.mli
@@ -48,6 +48,13 @@ val get_all: t -> lscope_var list
    The first element is the first [lscope_var] that was added to [t], the
    second element is the second [lscope_var] that was added to [t], an so on. *)
 
-val is_used: t -> Misc.pred_or_term -> bool
+type pred_or_term = PoT_pred of predicate | PoT_term of term
+val is_used: t -> pred_or_term -> bool
 (* [is_used lscope pot] returns [true] iff [pot] uses a variable from
    [lscope]. *)
+
+(*
+Local Variables:
+compile-command: "make -C ../../../../.."
+End:
+*)
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
index 59a6acb5cf95cc7762a67ebbb5af99c854579eed..040c83991edcca505c5758fdf0ad4dea40420c12 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
@@ -225,9 +225,9 @@ let to_exp ~loc kf env pot label =
   in
   (* Creating the pointer *)
   let ty = match pot with
-  | Misc.PoT_pred _ ->
+  | Lscope.PoT_pred _ ->
     Cil.intType
-  | Misc.PoT_term t ->
+  | Lscope.PoT_term t ->
     begin match Typing.get_number_ty t with
     | Typing.(C_integer _ | C_float _ | Nan) ->
       Typing.get_typ t
@@ -289,7 +289,7 @@ let to_exp ~loc kf env pot label =
     let term_to_exp = !term_to_exp_ref in
     let named_predicate_to_exp = !predicate_to_exp_ref in
     match pot with
-    | Misc.PoT_pred p ->
+    | Lscope.PoT_pred p ->
       let env = Env.push env in
       let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
       let e, env = named_predicate_to_exp kf env p in
@@ -303,7 +303,7 @@ let to_exp ~loc kf env pot label =
       (* We CANNOT return [block.bstmts] because it does NOT contain
         variable declarations. *)
       [ Constructor.mk_block_stmt block ], env
-    | Misc.PoT_term t ->
+    | Lscope.PoT_term t ->
       begin match Typing.get_number_ty t with
       | Typing.(C_integer _ | C_float _ | Nan) ->
         let env = Env.push env in
@@ -347,6 +347,6 @@ let to_exp ~loc kf env pot label =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)
diff --git a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
index 3b6dda222774a0cde05bdce183bc273ef75c4742..f5b51d739bd4de58a55583a2e68cd2f95696b87e 100644
--- a/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
+++ b/src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
@@ -32,7 +32,7 @@ open Cil_datatype
 
 val to_exp:
   loc:Location.t -> kernel_function -> Env.t ->
-  Misc.pred_or_term -> logic_label -> exp * Env.t
+  Lscope.pred_or_term -> logic_label -> exp * Env.t
 
 (*****************************************************************************)
 (**************************** Handling memory ********************************)
@@ -70,6 +70,6 @@ val term_to_exp_ref:
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 5c470efe5a0fa3014f8d418209daa1c74bf94417..66e129d1ce2df88cc78035f1d356baa29debc6b4 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -686,7 +686,7 @@ and context_insensitive_term_to_exp kf env t =
     e, env, C_number, ""
   | Tat(t', label) ->
     let lscope = Env.Logic_scope.get env in
-    let pot = Misc.PoT_term t' in
+    let pot = Lscope.PoT_term t' in
     if Lscope.is_used lscope pot then
       let e, env = At_with_lscope.to_exp ~loc kf env pot label in
       e, env, C_number, ""
@@ -947,7 +947,7 @@ and named_predicate_content_to_exp ?name kf env p =
     named_predicate_to_exp kf env p
   | Pat(p', label) ->
     let lscope = Env.Logic_scope.get env in
-    let pot = Misc.PoT_pred p' in
+    let pot = Lscope.PoT_pred p' in
     if Lscope.is_used lscope pot then
       At_with_lscope.to_exp ~loc kf env pot label
     else begin
diff --git a/src/plugins/e-acsl/src/libraries/misc.ml b/src/plugins/e-acsl/src/libraries/misc.ml
index 3ef0b0452028f3c97a11f0ac1373de59d6be88a6..0b2cd0d3ad79f9a6f08f442da392e7013fd38041 100644
--- a/src/plugins/e-acsl/src/libraries/misc.ml
+++ b/src/plugins/e-acsl/src/libraries/misc.ml
@@ -146,8 +146,6 @@ let term_has_lv_from_vi t =
   with Lv_from_vi_found ->
     true
 
-type pred_or_term = PoT_pred of predicate | PoT_term of term
-
 let mk_ptr_sizeof typ loc =
   match Cil.unrollType typ with
   | TPtr (t', _) -> Cil.new_exp ~loc (SizeOf t')
diff --git a/src/plugins/e-acsl/src/libraries/misc.mli b/src/plugins/e-acsl/src/libraries/misc.mli
index 1a66d8cf412a9c0c2ef315e7797ff7b26fa8627c..f9c92c19e8097a872a37edc83fa83301a79dd645 100644
--- a/src/plugins/e-acsl/src/libraries/misc.mli
+++ b/src/plugins/e-acsl/src/libraries/misc.mli
@@ -35,15 +35,11 @@ val result_vi: kernel_function -> varinfo
 (** @return the varinfo corresponding to \result in the given function *)
 
 (* ************************************************************************** *)
-(** {2 Handling the E-ACSL's C-libraries} *)
+(** {2 Other stuff} *)
 (* ************************************************************************** *)
 
 val is_fc_or_compiler_builtin: varinfo -> bool
 
-(* ************************************************************************** *)
-(** {2 Other stuff} *)
-(* ************************************************************************** *)
-
 val term_addr_of: loc:location -> term_lval -> typ -> term
 
 val cty: logic_type -> typ
@@ -72,8 +68,6 @@ val term_has_lv_from_vi: term -> bool
 (** @return true iff the given term contains a variables that originates from
     a C varinfo, that is a non-purely logic variable. *)
 
-type pred_or_term = PoT_pred of predicate | PoT_term of term
-
 val mk_ptr_sizeof: typ -> location -> exp
 (** [mk_ptr_sizeof ptr_typ loc] takes the pointer typ [ptr_typ] that points
     to a [typ] typ and returns [sizeof(typ)]. *)