diff --git a/src/ecEnv.ml b/src/ecEnv.ml
index b4e633dc6..ba9a04daa 100644
--- a/src/ecEnv.ml
+++ b/src/ecEnv.ml
@@ -184,6 +184,7 @@ type preenv = {
   env_atbase   : (path list Mint.t) Msym.t;
   env_redbase  : mredinfo;
   env_ntbase   : ntbase Mop.t;
+  env_albase   : path Mp.t;             (* theory aliases   *)
   env_modlcs   : Sid.t;                 (* declared modules *)
   env_item     : theory_item list;      (* in reverse order *)
   env_norm     : env_norm ref;
@@ -308,6 +309,7 @@ let empty gstate =
     env_atbase   = Msym.empty;
     env_redbase  = Mrd.empty;
     env_ntbase   = Mop.empty;
+    env_albase   = Mp.empty;
     env_modlcs   = Sid.empty;
     env_item     = [];
     env_norm     = ref empty_norm_cache;
@@ -2856,12 +2858,13 @@ module Theory = struct
     else
       Option.get (Mp.find_opt p env.env_thenvs)
 
-
   (* ------------------------------------------------------------------ *)
   let rebind_alias (name : symbol) (path : path) (env : env) =
     let th = by_path path env in
+    let src = EcPath.pqname (root env) name in
     let env = MC.import_theory ~name path th env in
     let env = MC.import_mc ~name (IPPath path) env in
+    let env = { env with env_albase = Mp.add path src env.env_albase } in
     env
 
   (* ------------------------------------------------------------------ *)
@@ -2870,6 +2873,10 @@ module Theory = struct
       if import.im_immediate then rebind_alias name path env else env in
     { env with env_item = mkitem import (Th_alias (name, path)) :: env.env_item }
 
+  (* ------------------------------------------------------------------ *)
+  let aliases (env : env) =
+    env.env_albase
+
   (* ------------------------------------------------------------------ *)
   let rec bind_instance_th path inst cth =
     List.fold_left (bind_instance_th_item path) inst cth
diff --git a/src/ecEnv.mli b/src/ecEnv.mli
index ef3780922..0d25b330f 100644
--- a/src/ecEnv.mli
+++ b/src/ecEnv.mli
@@ -295,6 +295,7 @@ module Theory : sig
     -> env -> compiled_theory option
 
   val alias : ?import:import -> symbol -> path -> env -> env
+  val aliases : env -> path Mp.t
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index bd86150c9..1995b5a86 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -143,7 +143,18 @@ module PPEnv = struct
             (fun env x -> EcEnv.Mod.bind_param x mty env)
             ppe.ppe_env xs; }
 
-  let p_shorten cond p =
+  let reverse_theory_alias (ppe : t) (path : P.path) : P.path =
+    let aliases = EcEnv.Theory.aliases ppe.ppe_env in
+
+    let rec reverse (suffix : symbol list) (p : P.path option) =
+      Option.bind p (fun prefix ->
+        match P.Mp.find_opt prefix aliases with
+        | None -> reverse (P.basename prefix :: suffix) (P.prefix prefix)
+        | Some prefix -> Some (EcPath.extend prefix suffix)
+      )
+    in Option.value ~default:path (reverse [] (Some path))
+
+  let p_shorten ?(istheory = false) (ppe : t) (cond : qsymbol -> bool) (p : P.path) =
     let rec shorten prefix (nm, x) =
       match cond (nm, x) with
       | true  -> (nm, x)
@@ -154,36 +165,43 @@ module PPEnv = struct
       end
     in
 
+    let p =
+      if istheory then
+        reverse_theory_alias ppe p
+      else
+        let thpath, base = P.prefix p, P.basename p in
+        let thpath = Option.map (reverse_theory_alias ppe) thpath in
+        P.pqoname thpath base in
     let (nm, x) = P.toqsymbol p in
     shorten (List.rev nm) ([], x)
 
   let ty_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.Ty.lookup_path ~unique:true sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let tc_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.TypeClass.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let rw_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.BaseRw.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let ax_symb (ppe : t) p =
-      let exists sm =
+    let exists sm =
       try  EcPath.p_equal (EcEnv.Ax.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let op_symb (ppe : t) p info =
     let specs = [1, EcPath.pqoname (EcPath.prefix EcCoreLib.CI_Bool.p_eq) "<>"] in
@@ -221,21 +239,21 @@ module PPEnv = struct
       (* FIXME: for special operators, do check `info` *)
       if   List.exists (fun (_, sp) -> EcPath.p_equal sp p) specs
       then ([], EcPath.basename p)
-      else p_shorten exists p
+      else p_shorten ppe exists p
 
   let ax_symb (ppe : t) p =
     let exists sm =
       try  EcPath.p_equal (EcEnv.Ax.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ppe exists p
 
   let th_symb (ppe : t) p =
     let exists sm =
       try  EcPath.p_equal (EcEnv.Theory.lookup_path sm ppe.ppe_env) p
       with EcEnv.LookupFailure _ -> false
     in
-      p_shorten exists p
+      p_shorten ~istheory:true ppe exists p
 
   let rec mod_symb (ppe : t) mp : EcSymbols.msymbol =
     let (nm, x, p2) =