diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index ea02461aaf259c7888056428fbac6ea9cf2d80c6..3328f6fde9e01194b8e63115401d66628f8525a4 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -658,12 +658,6 @@ sig
   val conditional_conversion:
     Cil_types.location -> Logic_ptree.relation option ->
     Cil_types.term -> Cil_types.term -> Cil_types.logic_type
-
-  val add_import : ?current:bool -> ?alias:string -> string -> unit
-  val clear_imports : unit -> unit
-  val push_imports : unit -> unit
-  val pop_imports : unit -> unit
-
   val term : Lenv.t -> Logic_ptree.lexpr -> term
   val predicate : Lenv.t -> Logic_ptree.lexpr -> predicate
   val code_annot :
@@ -735,14 +729,9 @@ struct
     | None -> !imported_scopes
     | Some s -> s :: !imported_scopes
 
-  let clear_imports () =
-    begin
-      Stack.clear scopes ;
-      current_scope := None ;
-      imported_scopes := [] ;
-    end
   let push_imports () =
     Stack.push (!current_scope,!imported_scopes) scopes
+
   let pop_imports () =
     begin
       let c,s = Stack.pop scopes in
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index 9af8714ecb2ca12f85a57bb16a813ff12c4c252b..83ed8d4baa63b547e4867f04d62762790c69d05e 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -181,12 +181,6 @@ sig
     Cil_types.location -> Logic_ptree.relation option ->
     Cil_types.term -> Cil_types.term -> Cil_types.logic_type
 
-  (** Open module in local environment. *)
-  val add_import : ?current:bool -> ?alias:string -> string -> unit
-  val clear_imports : unit -> unit
-  val push_imports : unit -> unit
-  val pop_imports : unit -> unit
-
   (** type-checks a term. *)
   val term : Lenv.t -> Logic_ptree.lexpr -> term