diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index b700d1f25efa1662e47788d857a541a854033f89..f2158c1dc0b543ef55aa170dfdfeb08d9acd0edb 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -758,7 +758,7 @@ struct
 
   let add_import ?(current=false) ?alias name =
     begin
-      let short = match alias with Some a -> a | None ->
+      let short = match alias with Some "_" -> "" | Some a -> a | None ->
         List.hd @@ List.rev @@ Logic_utils.longident name in
       let s = {
         long_prefix = name ^ "::";
@@ -4303,8 +4303,8 @@ struct
         C.error loc
           "Duplicated axiomatics %s (first occurrence at %a)"
           id Cil_printer.pp_location oldloc in
-      let l = List.filter_map (decl ~context:InAxiomatic) decls in
       ignore (Logic_env.Axiomatics.memo ~change (fun _ -> loc) id);
+      let l = List.filter_map (decl ~context:InAxiomatic) decls in
       Some (Daxiomatic(id,l,[],loc))
 
     | LDmodule(id,decls) ->
@@ -4320,23 +4320,29 @@ struct
         C.error loc
           "Duplicated module %s (first occurrence at %a)"
           id Cil_printer.pp_location oldloc in
+      ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
       push_imports () ;
       add_import ~current:true name ;
       let l = List.filter_map (decl ~context) decls in
       pop_imports () ;
-      ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
       Some (Dmodule(name,l,[],None,loc))
 
     | LDimport(None,name,alias) ->
       add_import ?alias name ; None
 
     | LDimport(Some driver as drv,name,alias) ->
-      let decls = ref [] in
-      let builder = make_module_builder decls name in
-      let path = Logic_utils.longident name in
-      Extensions.importer driver ~builder ~loc path ;
-      add_import ?alias name ;
-      Some (Dmodule(name,List.rev !decls,[],drv,loc))
+      let annot =
+        if not @@ Logic_env.Modules.mem name then
+          begin
+            let decls = ref [] in
+            let builder = make_module_builder decls name in
+            let path = Logic_utils.longident name in
+            Extensions.importer driver ~builder ~loc path ;
+            Logic_env.Modules.add name loc ;
+            Some (Dmodule(name,List.rev !decls,[],drv,loc))
+          end
+        else None
+      in add_import ?alias name ; annot
 
     | LDtype(name,l,def) ->
       let env = init_type_variables loc l in
diff --git a/tests/spec/import.i b/tests/spec/import.i
index 82ef19a692765cabf5d6293f7f1f51671ba5c874..837dffbac760fa5033558c9180fdd888069089e1 100644
--- a/tests/spec/import.i
+++ b/tests/spec/import.i
@@ -6,6 +6,8 @@ OPT: -print -kernel-msg-key printer:imported-modules
 
 /*@ import foo: A::B; */
 /*@ predicate check1(B::t x) = B::check(x,0); */
+/*@ predicate check2(A::B::t x) = A::B::check(x,0); */
 
-/* import foo: A::B \as C; */
-/* predicate check2(C::t x) = A::B::check(x,0); */
+/*@ import foo: A::B \as C; */
+/*@ predicate check3(C::t x) = C::check(x,0); */
+/*@ predicate check4(C::t x) = A::B::check(x,0); */
diff --git a/tests/spec/oracle/import.0.res.oracle b/tests/spec/oracle/import.0.res.oracle
index 22a7a7d111aa0dcd24c32997d22d4c4bc56f5e98..f0f5707e2ba6de2ef31dda0f96f9bc8b235a3fa2 100644
--- a/tests/spec/oracle/import.0.res.oracle
+++ b/tests/spec/oracle/import.0.res.oracle
@@ -7,4 +7,10 @@
  */
 /*@ predicate check1(A::B::t x) = A::B::check(x, 0);
  */
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */
 
diff --git a/tests/spec/oracle/import.1.res.oracle b/tests/spec/oracle/import.1.res.oracle
index 3a070d6021774a82c0688f837ace4aa5f910c9aa..b5236c1c99d2aa32e40c018dc31bfb639b8e0beb 100644
--- a/tests/spec/oracle/import.1.res.oracle
+++ b/tests/spec/oracle/import.1.res.oracle
@@ -13,4 +13,10 @@
  */
 /*@ predicate check1(A::B::t x) = A::B::check(x, 0);
  */
+/*@ predicate check2(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check3(A::B::t x) = A::B::check(x, 0);
+ */
+/*@ predicate check4(A::B::t x) = A::B::check(x, 0);
+ */