diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 541a190501de314af3413b116ec35a3d8e161279..e7f3e3ff6034f52f5fdb9f572988c1adb18615b7 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -715,7 +715,7 @@ struct
   (* Imported Scope *)
 
   type scope = {
-    current: bool; (* accepted for non-qualified names *)
+    unqualified: bool; (* accepted for non-qualified names *)
     long_prefix: string; (* last '::' included *)
     short_prefix: string; (* last '::' included *)
   }
@@ -730,8 +730,8 @@ struct
     | None -> !imported_scopes
     | Some s -> s :: !imported_scopes
 
-  let current_scopes () =
-    List.filter (fun s -> s.current) @@ all_scopes ()
+  let unqualified_scopes () =
+    List.filter (fun s -> s.unqualified) @@ all_scopes ()
 
   let push_imports () =
     let current = !current_scope in
@@ -763,7 +763,7 @@ struct
           List.hd @@ List.rev @@ Logic_utils.longident name
       in
       let s = {
-        current;
+        unqualified = current || alias = None;
         long_prefix = name ^ "::";
         short_prefix = short ^ "::";
       } in
@@ -787,7 +787,7 @@ struct
       in find_opt resolved_name
     else
       let find_in_scope s = find_opt (s.long_prefix ^ a) in
-      match List.find_map find_in_scope @@ current_scopes () with
+      match List.find_map find_in_scope @@ unqualified_scopes () with
       | None -> find_opt a
       | Some _ as result -> result
 
diff --git a/tests/spec/module.c b/tests/spec/module.c
index abf32bb5668dd6dbf57824ce83b9c9feaa66510b..6fa3d132da5e5acc9cf49cb54232485521ec6110 100644
--- a/tests/spec/module.c
+++ b/tests/spec/module.c
@@ -12,9 +12,34 @@
   }
   module foo::bar {
     import Foo \as X;
+    type a;
+    logic a f(a x);
     logic X::t inv(X::t x);
     logic X::t opN(X::t x, integer n) = n >= 0 ? X::opN(x,n) : opN(inv(x),-n);
   }
+  module foo::jazz {
+    import Foo; // both t and Foo::t can be used
+    type a;
+    logic a f(a x);
+    logic t inv(Foo::t x);
+    logic t opN(t x, integer n) = n >= 0 ? opN(x,n) : Foo::opN(inv(x),-n);
+  }
+  module priority {
+    import Foo ;
+    import foo::bar ;
+    import foo::jazz ;
+    logic t inv_jazz(t x) = inv(x); // OK, shall call foo::jazz::opN
+    logic a f_jazz(a x) = f(x);     // OK, shall call foo::jazz::f
+    logic bar::a f_bar(bar::a y) = bar::f(y); // OK
+  }
+  module priority_aliased {
+    import Foo ;
+    import foo::bar \as B;
+    import foo::jazz \as J;
+    logic t inv_jazz(t x) = J::inv(x);   // OK
+    logic J::a f_jazz(J::a x) = J::f(x); // OK
+    logic B::a f_bar (B::a y) = B::f(y); // OK
+  }
   import Foo \as A;
   import foo::bar \as B;
   lemma AbsOp: \forall Foo::t x, integer n;
@@ -24,7 +49,6 @@
 #ifdef ILL_TYPED
 
 /*@
-
   import Foo \as F;
   logic t x = F::e; // ill-formed: t should be F::t
 */
@@ -50,4 +74,13 @@ logic integer z = b::a; // KO
 
 */
 
+/*@
+  module wrong_priority {
+    import Foo ;
+    import foo::bar ;
+    import foo::jazz ;
+    logic a f_ko(a x) = bar::f(x);  // KO, ill typed
+  }
+ */
+
 #endif
diff --git a/tests/spec/oracle/module.0.res.oracle b/tests/spec/oracle/module.0.res.oracle
index 359107044c42293087ba7e00561478e7280aecd0..a09b766c3acab61ad73797fb42bb17fa8f4bd5b8 100644
--- a/tests/spec/oracle/module.0.res.oracle
+++ b/tests/spec/oracle/module.0.res.oracle
@@ -14,6 +14,10 @@ module Foo {
  */
 /*@
 module foo::bar {
+  type a;
+  
+  logic a f(a x) ;
+  
   logic Foo::t inv(Foo::t x) ;
   
   logic Foo::t opN(Foo::t x, ℤ n) =
@@ -22,6 +26,39 @@ module foo::bar {
   }
  */
 /*@
+module foo::jazz {
+  type a;
+  
+  logic a f(a x) ;
+  
+  logic Foo::t inv(Foo::t x) ;
+  
+  logic Foo::t opN(Foo::t x, ℤ n) =
+    n ≥ 0? opN(x, n): Foo::opN(inv(x), -n);
+  
+  }
+ */
+/*@
+module priority {
+  logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+  
+  logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+  
+  logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+  
+  }
+ */
+/*@
+module priority_aliased {
+  logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+  
+  logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+  
+  logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+  
+  }
+ */
+/*@
 lemma AbsOp:
   ∀ Foo::t x, ℤ n; foo::bar::opN(x, \abs(n)) ≡ Foo::opN(x, \abs(n));
  */
diff --git a/tests/spec/oracle/module.1.res.oracle b/tests/spec/oracle/module.1.res.oracle
index 85b7349dbe71a81252eeee8882a941511dd5a82f..b59f47ec8eac8cf2157e152182df5cb5a034f9e7 100644
--- a/tests/spec/oracle/module.1.res.oracle
+++ b/tests/spec/oracle/module.1.res.oracle
@@ -1,10 +1,12 @@
 [kernel] Parsing module.c (with preprocessing)
-[kernel:annot-error] module.c:29: Warning: 
+[kernel:annot-error] module.c:53: Warning: 
   no such type t. Ignoring global annotation
-[kernel:annot-error] module.c:36: Warning: 
+[kernel:annot-error] module.c:60: Warning: 
   unbound logic function bar::inv. Ignoring global annotation
-[kernel:annot-error] module.c:49: Warning: 
+[kernel:annot-error] module.c:73: Warning: 
   unbound logic variable b::a. Ignoring global annotation
+[kernel:annot-error] module.c:82: Warning: 
+  incompatible types foo::jazz::a and foo::bar::a. Ignoring global annotation
 /* Generated by Frama-C */
 /*@
 module Foo {
@@ -20,6 +22,10 @@ module Foo {
  */
 /*@
 module foo::bar {
+  type a;
+  
+  logic a f(a x) ;
+  
   logic Foo::t inv(Foo::t x) ;
   
   logic Foo::t opN(Foo::t x, ℤ n) =
@@ -28,6 +34,39 @@ module foo::bar {
   }
  */
 /*@
+module foo::jazz {
+  type a;
+  
+  logic a f(a x) ;
+  
+  logic Foo::t inv(Foo::t x) ;
+  
+  logic Foo::t opN(Foo::t x, ℤ n) =
+    n ≥ 0? opN(x, n): Foo::opN(inv(x), -n);
+  
+  }
+ */
+/*@
+module priority {
+  logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+  
+  logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+  
+  logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+  
+  }
+ */
+/*@
+module priority_aliased {
+  logic Foo::t inv_jazz(Foo::t x) = foo::jazz::inv(x);
+  
+  logic foo::jazz::a f_jazz(foo::jazz::a x) = foo::jazz::f(x);
+  
+  logic foo::bar::a f_bar(foo::bar::a y) = foo::bar::f(y);
+  
+  }
+ */
+/*@
 lemma AbsOp:
   ∀ Foo::t x, ℤ n; foo::bar::opN(x, \abs(n)) ≡ Foo::opN(x, \abs(n));
  */