diff --git a/src/lib/dune b/src/lib/dune
index f91c8ecea..0d8ecc3c6 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -57,7 +57,7 @@
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols
-    Expr Var Ty Typed Xliteral ModelMap Id Uid Objective Literal
+    Expr Var Ty Typed Xliteral ModelMap Id Objective Literal
     ; util
     Emap Gc_debug Hconsing Hstring Heap Loc Numbers Uqueue
     Options Timers Util Vec Version Steps Printer
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
index 8c885caac..afa71e83d 100644
--- a/src/lib/frontend/models.ml
+++ b/src/lib/frontend/models.ml
@@ -20,6 +20,7 @@ module Sy = Symbols
 module X = Shostak.Combine
 module E = Expr
 module MS = Map.Make(String)
+module DE = Dolmen.Std.Expr
 
 let constraints = ref MS.empty
 
@@ -110,15 +111,15 @@ module Pp_smtlib_term = struct
 
         | Sy.L_built (Sy.IsConstr hs), [e] ->
           if Options.get_output_smtlib () then
-            fprintf fmt "((_ is %a) %a)" Uid.pp hs print e
+            fprintf fmt "((_ is %a) %a)" DE.Term.Const.print hs print e
           else
-            fprintf fmt "(%a ? %a)" print e Uid.pp hs
+            fprintf fmt "(%a ? %a)" print e DE.Term.Const.print hs
 
         | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
           if Options.get_output_smtlib () then
-            fprintf fmt "(not ((_ is %a) %a))" Uid.pp hs print e
+            fprintf fmt "(not ((_ is %a) %a))" DE.Term.Const.print hs print e
           else
-            fprintf fmt "not (%a ? %a)" print e Uid.pp hs
+            fprintf fmt "not (%a ? %a)" print e DE.Term.Const.print hs
 
         | (Sy.L_built (Sy.LT | Sy.LE | Sy.BVULE)
           | Sy.L_neg_built (Sy.LT | Sy.LE | Sy.BVULE)
@@ -152,9 +153,9 @@ module Pp_smtlib_term = struct
 
     | Sy.Op (Sy.Access field), [e] ->
       if Options.get_output_smtlib () then
-        fprintf fmt "(%a %a)" Uid.pp field print e
+        fprintf fmt "(%a %a)" DE.Term.Const.print field print e
       else
-        fprintf fmt "%a.%a" print e Uid.pp field
+        fprintf fmt "%a.%a" print e DE.Term.Const.print field
 
     | Sy.Op (Sy.Record), _ ->
       begin match ty with
@@ -163,7 +164,7 @@ module Pp_smtlib_term = struct
           fprintf fmt "{";
           ignore (List.fold_left2 (fun first (field,_) e ->
               fprintf fmt "%s%a = %a"  (if first then "" else "; ")
-                Uid.pp field print e;
+                DE.Term.Const.print field print e;
               false
             ) true lbs xs);
           fprintf fmt "}";
@@ -178,7 +179,7 @@ module Pp_smtlib_term = struct
 
     (* TODO: introduce PrefixOp in the future to simplify this ? *)
     | Sy.Op (Sy.Constr hs), ((_::_) as l) ->
-      fprintf fmt "%a(%a)" Uid.pp hs print_list l
+      fprintf fmt "%a(%a)" DE.Term.Const.print hs print_list l
 
     | Sy.Op _, [e1; e2] ->
       if Options.get_output_smtlib () then
@@ -187,7 +188,7 @@ module Pp_smtlib_term = struct
         fprintf fmt "(%a %a %a)" print e1 Sy.print f print e2
 
     | Sy.Op Sy.Destruct hs, [e] ->
-      fprintf fmt "%a#%a" print e Uid.pp hs
+      fprintf fmt "%a#%a" print e DE.Term.Const.print hs
 
 
     | Sy.In(lb, rb), [t] ->
diff --git a/src/lib/frontend/translate.ml b/src/lib/frontend/translate.ml
index cd3da963c..95effbb55 100644
--- a/src/lib/frontend/translate.ml
+++ b/src/lib/frontend/translate.ml
@@ -237,7 +237,7 @@ let inject_ae_to_smt2 id =
         in
         {id with name}
       else
-        match Fpa_rounding.rounding_mode_of_ae_hs (Hstring.make n) with
+        match Fpa_rounding.rounding_mode_of_ae n with
         | rm ->
           let name =
             Dolmen_std.Name.simple (Fpa_rounding.string_of_rounding_mode rm)
@@ -580,7 +580,6 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
     (* Records and adts that only have one case are treated in the same way,
        and considered as records. *)
     Nest.attach_orders [adt];
-    let uid = Uid.of_ty_cst ty_c in
     let tyvl = Cache.store_ty_vars_ret id_ty in
     let lbs =
       Array.fold_right (
@@ -588,7 +587,7 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
           match c with
           | Some (DE.{ id_ty; _ } as id) ->
             let pty = dty_to_ty id_ty in
-            (Uid.of_term_cst id, pty) :: acc
+            (id, pty) :: acc
           | _ ->
             Fmt.failwith
               "Unexpected null label for some field of the record type %a"
@@ -596,15 +595,13 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
 
       ) dstrs []
     in
-    let record_constr = Uid.of_term_cst cstr in
-    let ty = Ty.trecord ~record_constr tyvl uid lbs in
+    let ty = Ty.trecord ~record_constr:cstr tyvl ty_c lbs in
     Cache.store_ty ty_c ty
 
   | Some (Adt { cases; _ } as adt) ->
     Nest.attach_orders [adt];
-    let uid = Uid.of_ty_cst ty_c in
     let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
-    Cache.store_ty ty_c (Ty.t_adt uid tyvl);
+    Cache.store_ty ty_c (Ty.t_adt ty_c tyvl);
     let cs =
       Array.fold_right (
         fun DE.{ cstr; dstrs; _ } accl ->
@@ -613,21 +610,21 @@ let mk_ty_decl (ty_c: DE.ty_cst) =
               fun tc_o acc ->
                 match tc_o with
                 | Some (DE.{ id_ty; _ } as field) ->
-                  (Uid.of_term_cst field, dty_to_ty id_ty) :: acc
+                  (field, dty_to_ty id_ty) :: acc
                 | None -> assert false
             ) dstrs []
           in
-          (Uid.of_term_cst cstr, fields) :: accl
+          (cstr, fields) :: accl
       ) cases []
     in
-    let ty = Ty.t_adt ~body:(Some cs) uid tyvl in
+    let ty = Ty.t_adt ~body:(Some cs) ty_c tyvl in
     Cache.store_ty ty_c ty
 
   | None | Some Abstract ->
     let ty_params = []
     (* List.init ty_c.id_ty.arity (fun _ -> Ty.fresh_tvar ()) *)
     in
-    let ty = Ty.text ty_params (Uid.of_ty_cst ty_c) in
+    let ty = Ty.text ty_params ty_c in
     Cache.store_ty ty_c ty
 
 (** Handles term declaration by storing the eventual present type variables
@@ -667,7 +664,7 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
             match c with
             | Some (DE.{ id_ty; _ } as id) ->
               let pty = dty_to_ty id_ty in
-              (Uid.of_term_cst id, pty) :: acc
+              (id, pty) :: acc
             | _ ->
               Fmt.failwith
                 "Unexpected null label for some field of the record type %a"
@@ -688,11 +685,11 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
                 fun tc_o acc ->
                   match tc_o with
                   | Some (DE.{ id_ty; _ } as id) ->
-                    (Uid.of_term_cst id, dty_to_ty id_ty) :: acc
+                    (id, dty_to_ty id_ty) :: acc
                   | None -> assert false
               ) dstrs []
             in
-            (Uid.of_term_cst cstr, fields) :: accl
+            (cstr, fields) :: accl
         ) cases []
       in
       let ty = Ty.t_adt ~body:(Some cs) hs tyl in
@@ -723,14 +720,13 @@ let mk_mr_ty_decls (tdl: DE.ty_cst list) =
         match tdef with
         | DE.Adt { cases; record; ty = ty_c; } as adt ->
           let tyvl = Cache.store_ty_vars_ret cases.(0).cstr.id_ty in
-          let uid = Uid.of_ty_cst ty_c in
-          let record_constr = Uid.of_term_cst cases.(0).cstr in
+          let record_constr = cases.(0).cstr in
           let ty =
             if (record || Array.length cases = 1) && not contains_adts
             then
-              Ty.trecord ~record_constr tyvl uid []
+              Ty.trecord ~record_constr tyvl ty_c []
             else
-              Ty.t_adt uid tyvl
+              Ty.t_adt ty_c tyvl
           in
           Cache.store_ty ty_c ty;
           (ty, Some adt) :: acc
@@ -748,14 +744,14 @@ let handle_patt_var id (DE.{ term_descr; _ } as term)  =
   match term_descr with
   | Cst ({ builtin = B.Base; id_ty; _ } as ty_c) ->
     let ty = dty_to_ty id_ty in
-    let v = Var.of_string @@ Uid.show id in
+    let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in
     let sy = Sy.Var v in
     Cache.store_sy ty_c sy;
     v, id, ty
 
   | Var ({ builtin = B.Base; id_ty; _ } as ty_v) ->
     let ty = dty_to_ty id_ty in
-    let v = Var.of_string @@ Uid.show id in
+    let v = Var.of_string @@ Fmt.str "%a" DE.Term.Const.print id in
     let sy = Sy.Var v in
     Cache.store_sy ty_v sy;
     v, id, ty
@@ -781,7 +777,7 @@ let mk_pattern DE.{ term_descr; _ } =
           Array.fold_right (
             fun v acc ->
               match v with
-              | Some dstr -> Uid.of_term_cst dstr :: acc
+              | Some dstr -> dstr :: acc
               | _ -> assert false
           ) dstrs []
         | _ ->
@@ -799,10 +795,10 @@ let mk_pattern DE.{ term_descr; _ } =
       ) [] vnames pargs
     in
     let args = List.rev rev_args in
-    Typed.Constr {name = Uid.of_term_cst cst; args}
+    Typed.Constr {name = cst; args}
 
   | Cst ({ builtin = B.Constructor _; _ } as cst) ->
-    Typed.Constr {name = Uid.of_term_cst cst; args = []}
+    Typed.Constr {name = cst; args = []}
 
   | Var ({ builtin = B.Base; path; _ } as t_v) ->
     (* Should the type be passed as an argument
@@ -924,7 +920,7 @@ let mk_add translate sy ty l =
   E.mk_term sy args ty
 
 let mk_rounding fpar =
-  let tcst = Uid.of_term_cst @@ Fpa_rounding.tcst_of_rounding_mode fpar in
+  let tcst = Fpa_rounding.tcst_of_rounding_mode fpar in
   let ty = Fpa_rounding.fpa_rounding_mode in
   E.mk_constr tcst [] ty
 
@@ -961,7 +957,7 @@ let rec mk_expr
               | Trecord _ as ty ->
                 E.mk_record [] ty
               | Tadt _ as ty ->
-                E.mk_constr (Uid.of_term_cst tcst) [] ty
+                E.mk_constr tcst [] ty
               | ty ->
                 Fmt.failwith "unexpected type %a@." Ty.print ty
             end
@@ -1006,9 +1002,9 @@ let rec mk_expr
                     let sy =
                       match Cache.find_ty adt with
                       | Trecord _ ->
-                        Sy.Op (Sy.Access (Uid.of_term_cst destr))
+                        Sy.Op (Sy.Access destr)
                       | Tadt _ ->
-                        Sy.destruct (Uid.of_term_cst destr)
+                        Sy.destruct destr
                       | _ -> assert false
                     in
                     E.mk_term sy [e] ty
@@ -1028,7 +1024,6 @@ let rec mk_expr
               cstr = { builtin = B.Constructor { adt; _ }; _ } as cstr; _
             }, [x] ->
             begin
-              let builtin = Sy.IsConstr (Uid.of_term_cst cstr) in
               let ty_c =
                 match DT.definition adt with
                 | Some (
@@ -1038,7 +1033,7 @@ let rec mk_expr
               in
               match Cache.find_ty ty_c with
               | Ty.Tadt _ ->
-                E.mk_builtin ~is_pos:true builtin [aux_mk_expr x]
+                E.mk_tester cstr (aux_mk_expr x)
 
               | Ty.Trecord _ ->
                 (* The typechecker allows only testers whose the
@@ -1314,7 +1309,7 @@ let rec mk_expr
             begin match ty with
               | Ty.Tadt _ ->
                 let l = List.map (fun t -> aux_mk_expr t) args in
-                E.mk_constr (Uid.of_term_cst tcst) l ty
+                E.mk_constr tcst l ty
               | Ty.Trecord _ ->
                 let l = List.map (fun t -> aux_mk_expr t) args in
                 E.mk_record l ty
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 9c443c0f7..fca71829f 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -27,20 +27,21 @@
 
 module Sy = Symbols
 module E  = Expr
+module DE = Dolmen.Std.Expr
 
 let src = Logs.Src.create ~doc:"Adt" __MODULE__
 module Log = (val Logs.src_log src : Logs.LOG)
 
 type 'a abstract =
   | Constr of {
-      c_name : Uid.term_cst;
+      c_name : DE.term_cst;
       c_ty : Ty.t;
-      c_args : (Uid.term_cst * 'a) list
+      c_args : (DE.term_cst * 'a) list
     }
   (* [Cons { c_name; c_ty; c_args }] reprensents the application of the
      constructor [c_name] of the ADT [ty] with the arguments [c_args]. *)
 
-  | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a }
+  | Select of { d_name : DE.term_cst ; d_ty : Ty.t ; d_arg : 'a }
   (* [Select { d_name; d_ty; d_arg }] represents the destructor [d_name] of
      the ADT [d_ty] on the ADT value [d_arg]. *)
 
@@ -67,7 +68,7 @@ let constr_of_destr ty dest =
       try
         List.find
           (fun { Ty.destrs; _ } ->
-             List.exists (fun (d, _) -> Uid.equal dest d) destrs
+             List.exists (fun (d, _) -> DE.Term.Const.equal dest d) destrs
           ) cases
       with Not_found -> assert false (* invariant *)
     end
@@ -105,7 +106,7 @@ module Shostak (X : ALIEN) = struct
     | None -> Alien r
 
   let pp_field ppf (lbl, v) =
-    Fmt.pf ppf "%a : %a" Uid.pp lbl X.print v
+    Fmt.pf ppf "%a : %a" DE.Term.Const.print lbl X.print v
 
   let print ppf = function
     | Alien x ->
@@ -113,11 +114,11 @@ module Shostak (X : ALIEN) = struct
 
     | Constr { c_name; c_args; _ } ->
       Fmt.pf ppf "%a@[(%a@])"
-        Uid.pp c_name
+        DE.Term.Const.print c_name
         Fmt.(list ~sep:semi pp_field) c_args
 
     | Select d ->
-      Fmt.pf ppf "%a#!!%a" X.print d.d_arg Uid.pp d.d_name
+      Fmt.pf ppf "%a#!!%a" X.print d.d_arg DE.Term.Const.print d.d_name
 
 
   let is_mine u =
@@ -131,7 +132,8 @@ module Shostak (X : ALIEN) = struct
       match embed d_arg with
       | Constr c ->
         begin
-          try snd @@ List.find (fun (lbl, _) -> Uid.equal d_name lbl) c.c_args
+          try snd @@ List.find
+              (fun (lbl, _) -> DE.Term.Const.equal d_name lbl) c.c_args
           with Not_found ->
             Printer.print_err "is_mine %a failed" print u;
             assert false
@@ -142,13 +144,13 @@ module Shostak (X : ALIEN) = struct
     match s1, s2 with
     | Alien r1, Alien r2 -> X.equal r1 r2
     | Constr c1, Constr c2 ->
-      Uid.equal c1.c_name c2.c_name &&
+      DE.Term.Const.equal c1.c_name c2.c_name &&
       Ty.equal c1.c_ty c2.c_ty &&
       begin
         try
           List.iter2
             (fun (hs1, v1) (hs2, v2) ->
-               assert (Uid.equal hs1 hs2);
+               assert (DE.Term.Const.equal hs1 hs2);
                if not (X.equal v1 v2) then raise Exit
             ) c1.c_args c2.c_args;
           true
@@ -158,7 +160,7 @@ module Shostak (X : ALIEN) = struct
       end
 
     | Select d1, Select d2 ->
-      Uid.equal d1.d_name d2.d_name &&
+      DE.Term.Const.equal d1.d_name d2.d_name &&
       Ty.equal d1.d_ty d2.d_ty &&
       X.equal d1.d_arg d2.d_arg
 
@@ -214,10 +216,10 @@ module Shostak (X : ALIEN) = struct
     | Constr { c_name ; c_ty ; c_args } ->
       List.fold_left
         (fun acc (_, r) -> acc * 7 + X.hash r)
-        (Uid.hash c_name + 7 * Ty.hash c_ty) c_args
+        (DE.Term.Const.hash c_name + 7 * Ty.hash c_ty) c_args
 
     | Select { d_name ; d_ty ; d_arg } ->
-      ((Uid.hash d_name + 11 * Ty.hash d_ty)) * 11 + X.hash d_arg
+      ((DE.Term.Const.hash d_name + 11 * Ty.hash d_ty)) * 11 + X.hash d_arg
 
   let leaves r =
     match r with
@@ -263,7 +265,7 @@ module Shostak (X : ALIEN) = struct
     | _, Alien _ -> -1
 
     | Constr c1, Constr c2 ->
-      let c = Uid.compare c1.c_name c2.c_name in
+      let c = DE.Term.Const.compare c1.c_name c2.c_name in
       if c <> 0 then c
       else
         let c = Ty.compare c1.c_ty c2.c_ty in
@@ -273,7 +275,7 @@ module Shostak (X : ALIEN) = struct
             try
               List.iter2
                 (fun (hs1, v1) (hs2, v2) ->
-                   assert (Uid.equal hs1 hs2);
+                   assert (DE.Term.Const.equal hs1 hs2);
                    let c = X.str_cmp v1 v2 in
                    if c <> 0 then raise (Util.Cmp c);
                 )c1.c_args c2.c_args;
@@ -286,7 +288,7 @@ module Shostak (X : ALIEN) = struct
     | _, Constr _ -> -1
 
     | Select d1, Select d2 ->
-      let c = Uid.compare d1.d_name d2.d_name in
+      let c = DE.Term.Const.compare d1.d_name d2.d_name in
       if c <> 0 then c
       else
         let c = Ty.compare d1.d_ty d2.d_ty in
@@ -378,13 +380,14 @@ module Shostak (X : ALIEN) = struct
       Sig.{ pb with sbt = (r, r1) :: pb.sbt }
 
     | Constr c1, Constr c2 ->
-      if not (Uid.equal c1.c_name c2.c_name) then raise Util.Unsolvable;
+      if not (DE.Term.Const.equal c1.c_name c2.c_name) then
+        raise Util.Unsolvable;
       try
         Sig.{pb with
              eqs =
                List.fold_left2
                  (fun eqs (hs1, v1) (hs2, v2) ->
-                    assert (Uid.equal hs1 hs2);
+                    assert (DE.Term.Const.equal hs1 hs2);
                     (v1, v2) :: eqs
                  )pb.eqs c1.c_args c2.c_args
             }
diff --git a/src/lib/reasoners/adt.mli b/src/lib/reasoners/adt.mli
index 2cd25de23..e81e50c05 100644
--- a/src/lib/reasoners/adt.mli
+++ b/src/lib/reasoners/adt.mli
@@ -29,12 +29,12 @@ val src : Logs.src
 
 type 'a abstract =
   | Constr of {
-      c_name : Uid.term_cst;
+      c_name : Dolmen.Std.Expr.term_cst;
       c_ty : Ty.t;
-      c_args : (Uid.term_cst * 'a) list
+      c_args : (Dolmen.Std.Expr.term_cst * 'a) list
     }
 
-  | Select of { d_name : Uid.term_cst ; d_ty : Ty.t ; d_arg : 'a }
+  | Select of { d_name : Dolmen.Std.Expr.term_cst ; d_ty : Ty.t ; d_arg : 'a }
 
   | Alien of 'a
 
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 91a37ecec..25a159b1f 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -46,7 +46,7 @@ module Log = (val Logs.src_log src : Logs.LOG)
 module TSet =
   Set.Make
     (struct
-      type t = Uid.term_cst
+      type t = DE.term_cst
 
       (* We use a dedicated total order on the constructors to ensure
          the termination of model generation. *)
@@ -113,7 +113,7 @@ module Domain = struct
 
   let pp ppf d =
     Fmt.(braces @@
-         iter ~sep:comma TSet.iter Uid.pp) ppf d.constrs;
+         iter ~sep:comma TSet.iter DE.Term.Const.print) ppf d.constrs;
     if Options.(get_verbose () || get_unsat_core ()) then
       Fmt.pf ppf " %a" (Fmt.box Ex.print) d.ex
 
@@ -173,7 +173,7 @@ module Domains = struct
      destructors of the constructor [c] by searching in the list [cases].
 
      A better predicate will be easy to implement after getting rid of
-     the legacy frontend and switching from [Uid.t] to
+     the legacy frontend and switching from [DE.t] to
      [Dolmen.Std.Expr.term_cst] to store the constructors. Indeed, [term_cst]
      contains the type of constructor and in particular its arity. *)
   let is_enum_constr r c =
@@ -270,7 +270,7 @@ let calc_destructor d e uf =
   let r, ex = Uf.find uf e in
   match Th.embed r with
   | Constr { c_args; _ } ->
-    begin match My_list.assoc Uid.equal d c_args with
+    begin match My_list.assoc DE.Term.Const.equal d c_args with
       | v -> Some (v, ex)
       | exception Not_found -> None
     end
@@ -559,7 +559,7 @@ let constr_of_destr ty d =
         let r =
           List.find
             (fun Ty.{ destrs; _ } ->
-               List.exists (fun (d', _) -> Uid.equal d d') destrs
+               List.exists (fun (d', _) -> DE.Term.Const.equal d d') destrs
             ) cases
         in
         r.constr
@@ -568,7 +568,7 @@ let constr_of_destr ty d =
 
   | _ -> assert false
 
-exception Found of X.r * Uid.term_cst
+exception Found of X.r * DE.term_cst
 
 let can_split env n =
   let m = Options.get_max_split () in
diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml
index cb8e11700..bc6c2a452 100644
--- a/src/lib/reasoners/records.ml
+++ b/src/lib/reasoners/records.ml
@@ -27,10 +27,11 @@
 
 module E = Expr
 module Sy = Symbols
+module DE = Dolmen.Std.Expr
 
 type 'a abstract =
-  | Record of (Uid.term_cst * 'a abstract) list * Ty.t
-  | Access of Uid.term_cst * 'a abstract * Ty.t
+  | Record of (DE.term_cst * 'a abstract) list * Ty.t
+  | Access of DE.term_cst * 'a abstract * Ty.t
   | Other of 'a * Ty.t
 
 module type ALIEN = sig
@@ -59,12 +60,12 @@ module Shostak (X : ALIEN) = struct
         let _ = List.fold_left
             (fun first (lb, e) ->
                Format.fprintf fmt "%s%a = %a"
-                 (if first then "" else "; ") Uid.pp lb print e;
+                 (if first then "" else "; ") DE.Term.Const.print lb print e;
                false
             ) true lbs in
         Format.fprintf fmt "}"
       | Access(a, e, _) ->
-        Format.fprintf fmt "%a.%a" print e Uid.pp a
+        Format.fprintf fmt "%a.%a" print e DE.Term.Const.print a
       | Other(t, _) -> X.print fmt t
 
   end
@@ -79,11 +80,11 @@ module Shostak (X : ALIEN) = struct
       if c <> 0 then c else X.str_cmp u1 u2
     | Other _, _ -> -1
     | _, Other _ -> 1
-    | Access (s1, u1, ty1), Access (s2, u2, ty2) ->
+    | Access (tcst1, u1, ty1), Access (tcst2, u2, ty2) ->
       let c = Ty.compare ty1 ty2 in
       if c <> 0 then c
       else
-        let c = Uid.compare s1 s2 in
+        let c = DE.Term.Const.compare tcst1 tcst2 in
         if c <> 0 then c
         else raw_compare u1 u2
     | Access _, _ -> -1
@@ -107,11 +108,11 @@ module Shostak (X : ALIEN) = struct
       begin
         let lbs_n = List.map (fun (lb, x) -> lb, normalize x) lbs in
         match lbs_n with
-        | (lb1, Access(lb2, x, _)) :: l when Uid.equal lb1 lb2 ->
+        | (lb1, Access(lb2, x, _)) :: l when DE.Term.Const.equal lb1 lb2 ->
           if List.for_all
               (function
                 | (lb1, Access(lb2, y, _)) ->
-                  Uid.equal lb1 lb2 && raw_compare x y = 0
+                  DE.Term.Const.equal lb1 lb2 && raw_compare x y = 0
                 | _ -> false) l
           then x
           else Record (lbs_n, ty)
@@ -120,7 +121,7 @@ module Shostak (X : ALIEN) = struct
     | Access (a, x, ty) ->
       begin
         match normalize x with
-        | Record (lbs, _) -> My_list.assoc Uid.equal a lbs
+        | Record (lbs, _) -> My_list.assoc DE.Term.Const.equal a lbs
         | x_n -> Access (a, x_n, ty)
       end
     | Other _ -> v
@@ -140,7 +141,7 @@ module Shostak (X : ALIEN) = struct
       Ty.equal ty1 ty2 && X.equal u1 u2
 
     | Access (s1, u1, ty1), Access (s2, u2, ty2) ->
-      Uid.equal s1 s2 && Ty.equal ty1 ty2 && equal u1 u2
+      DE.Term.Const.equal s1 s2 && Ty.equal ty1 ty2 && equal u1 u2
 
     | Record (lbs1, ty1), Record (lbs2, ty2) ->
       Ty.equal ty1 ty2 && equal_list lbs1 lbs2
@@ -225,10 +226,10 @@ module Shostak (X : ALIEN) = struct
   let rec hash  = function
     | Record (lbs, ty) ->
       List.fold_left
-        (fun h (lb, x) -> 17 * hash x + 13 * Uid.hash lb + h)
+        (fun h (lb, x) -> 17 * hash x + 13 * DE.Term.Const.hash lb + h)
         (Ty.hash ty) lbs
     | Access (a, x, ty) ->
-      19 * hash x + 17 * Uid.hash a + Ty.hash ty
+      19 * hash x + 17 * DE.Term.Const.hash a + Ty.hash ty
     | Other (x, ty) ->
       Ty.hash ty + 23 * X.hash x
 
@@ -367,10 +368,10 @@ module Shostak (X : ALIEN) = struct
     | Record (l1, _), Record (l2, _) ->
       let eqs =
         List.fold_left2
-          (fun eqs (a,b) (x,y) ->
-             assert (Uid.compare a x = 0);
+          (fun eqs (a, b) (x, y) ->
+             assert (DE.Term.Const.compare a x = 0);
              (is_mine y, is_mine b) :: eqs
-          )pb.eqs l1 l2
+          ) pb.eqs l1 l2
       in
       {pb with eqs=eqs}
 
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index 1693c209c..ad9ad7962 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -31,6 +31,7 @@ module E = Expr
 module A = Xliteral
 module LR = Uf.LX
 module SE = Expr.Set
+module DE = Dolmen.Std.Expr
 
 module Sy = Symbols
 
@@ -153,6 +154,8 @@ module Main_Default : S = struct
            | _ -> mp
         ) st Hstring.Map.empty
 
+    module Ty_map = Map.Make (DE.Ty.Const)
+
     let types_of_assumed sty =
       let open Ty in
       Ty.Set.fold
@@ -162,25 +165,25 @@ module Main_Default : S = struct
            | Tvar _ -> assert false
 
            | Text (_, hs) | Trecord { name = hs; _ } when
-               Uid.Ty_map.mem hs mp -> mp
+               Ty_map.mem hs mp -> mp
 
            | Text (l, hs) ->
              let l = List.map (fun _ -> Ty.fresh_tvar()) l in
-             Uid.Ty_map.add hs (Text(l, hs)) mp
+             Ty_map.add hs (Text(l, hs)) mp
 
            | Trecord { name; _ } ->
              (* cannot do better for records ? *)
-             Uid.Ty_map.add name ty mp
+             Ty_map.add name ty mp
 
            | Tadt (hs, _) ->
              (* cannot do better for ADT ? *)
-             Uid.Ty_map.add hs ty mp
-        )sty Uid.Ty_map.empty
+             Ty_map.add hs ty mp
+        )sty Ty_map.empty
 
     let print_types_decls ?(header=true) types =
       let open Ty in
       print_dbg ~flushed:false ~header "@[<v 2>(* types decls: *)@ ";
-      Uid.Ty_map.iter
+      Ty_map.iter
         (fun _ ty ->
            match ty with
            | Tint | Treal | Tbool | Tbitv _ | Tfarray _ -> ()
@@ -193,10 +196,10 @@ module Main_Default : S = struct
                | (lbl, ty)::l ->
                  let print fmt (lbl,ty) =
                    Format.fprintf fmt " ; %a :%a"
-                     Uid.pp lbl Ty.print ty in
+                     DE.Term.Const.print lbl Ty.print ty in
                  print_dbg ~flushed:false ~header:false
                    "{ %a : %a%a"
-                   Uid.pp lbl Ty.print ty
+                   DE.Term.Const.print lbl Ty.print ty
                    (pp_list_no_space print) l;
                  print_dbg ~flushed:false ~header:false " }@ "
              end
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index 2cd2be58e..6ed300d81 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -26,6 +26,7 @@
 (**************************************************************************)
 
 module Sy = Symbols
+module DE = Dolmen.Std.Expr
 
 (** Data structures *)
 
@@ -416,11 +417,11 @@ module SmtPrinter = struct
       Fmt.pf ppf "@[<2>(not@ %a@])" pp a
 
     | Sy.L_built (Sy.IsConstr hs), [e] ->
-      Fmt.pf ppf "@[<2>((_ is %a)@ %a@])" Uid.pp hs pp e
+      Fmt.pf ppf "@[<2>((_ is %a)@ %a@])" DE.Term.Const.print hs pp e
 
     | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
       Fmt.pf ppf "(not @[<2>((_ is %a)@ %a@]))"
-        Uid.pp hs pp e
+        DE.Term.Const.print hs pp e
 
     | (Sy.L_built (Sy.LT | Sy.LE | Sy.BVULE)
       | Sy.L_neg_built (Sy.LT | Sy.LE | Sy.BVULE)
@@ -449,7 +450,7 @@ module SmtPrinter = struct
         | Ty.Trecord { Ty.lbs = lbs; record_constr; _ } ->
           assert (List.compare_lengths xs lbs = 0);
           Fmt.pf ppf "@[<2>(%a %a@])"
-            Uid.pp record_constr
+            DE.Term.Const.print record_constr
             Fmt.(list ~sep:sp pp |> box) xs
 
         | _ ->
@@ -605,10 +606,10 @@ module AEPrinter = struct
       Fmt.pf ppf "(not %a)" pp a
 
     | Sy.L_built (Sy.IsConstr hs), [e] ->
-      Fmt.pf ppf "(%a ? %a)" pp e Uid.pp hs
+      Fmt.pf ppf "(%a ? %a)" pp e DE.Term.Const.print hs
 
     | Sy.L_neg_built (Sy.IsConstr hs), [e] ->
-      Fmt.pf ppf "not (%a ? %a)" pp e Uid.pp hs
+      Fmt.pf ppf "not (%a ? %a)" pp e DE.Term.Const.print hs
 
     | (Sy.L_built (Sy.LT | Sy.LE | Sy.BVULE)
       | Sy.L_neg_built (Sy.LT | Sy.LE | Sy.BVULE)
@@ -646,7 +647,7 @@ module AEPrinter = struct
       Fmt.pf ppf "%a^{%d, %d}" pp e i j
 
     | Sy.(Op (Access field)), [e] ->
-      Fmt.pf ppf "%a.%a" pp e Uid.pp field
+      Fmt.pf ppf "%a.%a" pp e DE.Term.Const.print field
 
     | Sy.(Op Record), _ ->
       begin match ty with
@@ -655,7 +656,7 @@ module AEPrinter = struct
           Fmt.pf ppf "{";
           ignore (List.fold_left2 (fun first (field,_) e ->
               Fmt.pf ppf "%s%a = %a"  (if first then "" else "; ")
-                Uid.pp field pp e;
+                DE.Term.Const.print field pp e;
               false
             ) true lbs xs);
           Fmt.pf ppf "}";
@@ -673,7 +674,7 @@ module AEPrinter = struct
 
     | Sy.(Op Destruct hs), [e] ->
       Fmt.pf ppf "%a#%a"
-        pp e Uid.pp hs
+        pp e DE.Term.Const.print hs
 
     | Sy.Op op, [e1; e2] ->
       Fmt.pf ppf "(%a %a %a)" pp e1 Symbols.pp_ae_operator op pp e2
@@ -1305,9 +1306,7 @@ let mk_tester cons t =
 
 let mk_record xs ty = mk_term (Sy.Op Record) xs ty
 
-let void =
-  let constr = Uid.of_term_cst Dolmen.Std.Expr.Term.Cstr.void in
-  mk_constr constr [] Ty.tunit
+let void = mk_constr Dolmen.Std.Expr.Term.Cstr.void [] Ty.tunit
 
 (** Substitutions *)
 
@@ -2033,7 +2032,7 @@ module Triggers = struct
 
     | { f = Op (Access a1) ; xs=[t1]; _ },
       { f = Op (Access a2) ; xs=[t2]; _ } ->
-      let c = Uid.compare a1 a2 in
+      let c = DE.Term.Const.compare a1 a2 in
       if c<>0 then c else cmp_trig_term t1 t2
 
     | { f = Op (Access _); _ }, _ -> -1
@@ -2041,7 +2040,7 @@ module Triggers = struct
 
     | { f = Op (Destruct a1) ; xs = [t1]; _ },
       { f = Op (Destruct a2) ; xs = [t2]; _ } ->
-      let c = Uid.compare a1 a2 in
+      let c = DE.Term.Const.compare a1 a2 in
       if c<>0 then c else cmp_trig_term t1 t2
 
     | { f = Op (Destruct _); _ }, _ -> -1
@@ -2645,7 +2644,7 @@ let debug_compile_match e cases res =
          | Typed.Constr {name; args} ->
            Printer.print_dbg  ~flushed:false ~header:false
              "| %a %a -> %a@ "
-             Uid.pp name
+             DE.Term.Const.print name
              p_list_vars args
              print v;
          | Typed.Var x ->
@@ -2948,8 +2947,8 @@ let const_view t =
     end
   | { f = Op (Constr c); ty; _ }
     when Ty.equal ty Fpa_rounding.fpa_rounding_mode ->
-    let c = Uid.show c |> Hstring.make in
-    RoundingMode (Fpa_rounding.rounding_mode_of_smt_hs c)
+    let c = Fmt.str "%a" DE.Term.Const.print c in
+    RoundingMode (Fpa_rounding.rounding_mode_of_smt c)
   | _ -> Fmt.failwith "unsupported constant: %a" print t
 
 let int_view t =
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index 7b30236e4..3204ca936 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -284,8 +284,8 @@ val mk_ite : t -> t -> t -> t
 
 (** smart constructor for datatypes. *)
 
-val mk_constr : Uid.term_cst -> t list -> Ty.t -> t
-val mk_tester : Uid.term_cst -> t -> t
+val mk_constr : Dolmen.Std.Expr.term_cst -> t list -> Ty.t -> t
+val mk_tester : Dolmen.Std.Expr.term_cst -> t -> t
 val mk_record : t list -> Ty.t -> t
 
 (** Substitutions *)
diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml
index bfb0a4174..194a5730e 100644
--- a/src/lib/structures/fpa_rounding.ml
+++ b/src/lib/structures/fpa_rounding.ml
@@ -27,7 +27,6 @@
 
 module DStd = Dolmen.Std
 module DE = DStd.Expr
-module Hs = Hstring
 module Q = Numbers.Q
 module Z = Numbers.Z
 
@@ -66,7 +65,6 @@ let to_ae_string = function
   | Down -> "Down"
   | NearestTiesToAway -> "NearestTiesToAway"
 
-
 let fpa_rounding_mode_ae_type_name = "fpa_rounding_mode"
 
 let fpa_rounding_mode_type_name = "RoundingMode"
@@ -74,14 +72,14 @@ let fpa_rounding_mode_type_name = "RoundingMode"
 (* The exported 'to string' function is the SMT one. *)
 let string_of_rounding_mode = to_smt_string
 
-let hstring_smt_reprs =
+let string_smt_reprs =
   List.map
     (fun c -> to_smt_string c, [])
     constrs
 
-let hstring_ae_reprs =
+let string_ae_reprs =
   List.map
-    (fun c -> Hs.make (to_ae_string c))
+    (fun c -> to_ae_string c)
     constrs
 
 let get_basename = function
@@ -113,8 +111,8 @@ let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode =
     def, constrs
   in
   Nest.attach_orders [def];
-  let body = List.map (fun c -> Uid.of_term_cst c, []) d_constrs in
-  let ty = Ty.t_adt ~body:(Some body) (Uid.of_ty_cst ty_cst) [] in
+  let body = List.map (fun c -> c, []) d_constrs in
+  let ty = Ty.t_adt ~body:(Some body) ty_cst [] in
   let tcst_of_rounding_mode m =
     let name = string_of_rounding_mode m in
     let opt =
@@ -129,37 +127,37 @@ let fpa_rounding_mode_dty, d_constrs, fpa_rounding_mode, tcst_of_rounding_mode =
   in
   DE.Ty.apply ty_cst [], d_constrs, ty, tcst_of_rounding_mode
 
-let rounding_mode_of_smt_hs =
+let rounding_mode_of_smt =
   let table = Hashtbl.create 5 in
   List.iter2 (
     fun (key, _) bnd ->
       Hashtbl.add table key bnd
-  ) hstring_smt_reprs constrs;
+  ) string_smt_reprs constrs;
   fun key ->
-    try Hashtbl.find table (Hstring.view key) with
+    try Hashtbl.find table key with
     | Not_found ->
       Fmt.failwith
-        "Error while searching for SMT2 FPA value %a."
-        Hstring.print key
+        "Error while searching for SMT2 FPA value %s."
+        key
         fpa_rounding_mode_type_name
 
-let rounding_mode_of_ae_hs =
+let rounding_mode_of_ae =
   let table = Hashtbl.create 5 in
   List.iter2 (
     fun key bnd ->
       Hashtbl.add table key bnd
-  ) hstring_ae_reprs constrs;
-  fun key ->
+  ) string_ae_reprs constrs;
+  fun (key : string) ->
     try Hashtbl.find table key with
     | Not_found ->
       Fmt.failwith
-        "Error while searching for Legacy FPA value %a."
-        Hstring.print key
+        "Error while searching for Legacy FPA value %s."
+        key
         fpa_rounding_mode_type_name
 
 let translate_smt_rounding_mode hs =
-  match rounding_mode_of_smt_hs hs with
-  | res -> Some (Hstring.make (to_ae_string res))
+  match rounding_mode_of_smt hs with
+  | res -> Some (to_ae_string res)
   | exception (Failure _) -> None
 
 (** Helper functions **)
diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli
index 6b0a14557..ed032e196 100644
--- a/src/lib/structures/fpa_rounding.mli
+++ b/src/lib/structures/fpa_rounding.mli
@@ -51,21 +51,21 @@ val fpa_rounding_mode_ae_type_name : string
 val fpa_rounding_mode_dty : Dolmen.Std.Expr.Ty.t
 
 (** The Dolmen constructors of [rounding_mode]. *)
-val d_constrs : Uid.DE.term_cst list
+val d_constrs : DE.term_cst list
 
 (** The rounding mode type. *)
 val fpa_rounding_mode : Ty.t
 
-(** Transforms the Hstring corresponding to a RoundingMode element into
+(** Transforms the string corresponding to a RoundingMode element into
     the [rounding_mode] equivalent. Raises 'Failure' if the string does not
     correspond to a valid rounding mode. *)
-val rounding_mode_of_smt_hs : Hstring.t -> rounding_mode
+val rounding_mode_of_smt : string -> rounding_mode
 
 (** Same, but for legacy's [rounding_mode] equivalent. *)
-val rounding_mode_of_ae_hs : Hstring.t -> rounding_mode
+val rounding_mode_of_ae : string -> rounding_mode
 
 (** Same, but from AE modes to SMT2 modes. *)
-val translate_smt_rounding_mode : Hstring.t -> Hstring.t option
+val translate_smt_rounding_mode : string -> string option
 
 (** Returns the string representation of the [rounding_mode] (SMT2 standard) *)
 val string_of_rounding_mode : rounding_mode -> string
diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml
index 902d33f94..87e47fb45 100644
--- a/src/lib/structures/symbols.ml
+++ b/src/lib/structures/symbols.ml
@@ -25,9 +25,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module DE = Dolmen.Std.Expr
+
 type builtin =
     LE | LT (* arithmetic *)
-  | IsConstr of Uid.term_cst (* ADT tester *)
+  | IsConstr of DE.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type operator =
@@ -35,9 +37,9 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Uid.term_cst | Record
-  | Constr of Uid.term_cst (* enums, adts *)
-  | Destruct of Uid.term_cst
+  | Access of DE.term_cst | Record
+  | Constr of DE.term_cst (* enums, adts *)
+  | Destruct of DE.term_cst
   (* Arrays *)
   | Get | Set
   (* BV *)
@@ -188,7 +190,7 @@ let compare_operators op1 op2 =
     (function
       | Access h1, Access h2 | Constr h1, Constr h2
       | Destruct h1, Destruct h2 ->
-        Uid.compare h1 h2
+        DE.Term.Const.compare h1 h2
       | Extract (i1, j1), Extract (i2, j2) ->
         let r = Int.compare i1 i2 in
         if r = 0 then Int.compare j1 j2 else r
@@ -213,7 +215,7 @@ let compare_operators op1 op2 =
 let compare_builtin b1 b2 =
   Util.compare_algebraic b1 b2
     (function
-      | IsConstr h1, IsConstr h2 -> Uid.compare h1 h2
+      | IsConstr tcst1, IsConstr tcst2 -> DE.Term.Const.compare tcst1 tcst2
       | _, (LT | LE | BVULE | IsConstr _) -> assert false
     )
 
@@ -379,9 +381,9 @@ module AEPrinter = struct
 
     (* DT theory *)
     | Record -> Fmt.pf ppf "@Record"
-    | Access s -> Fmt.pf ppf "@Access_%a" Uid.pp s
-    | Constr s
-    | Destruct s -> Uid.pp ppf s
+    | Access tcst -> Fmt.pf ppf "@Access_%a" DE.Term.Const.print tcst
+    | Constr tcst
+    | Destruct tcst -> DE.Term.Const.print ppf tcst
 
     (* Float theory *)
     | Float -> Fmt.pf ppf "float"
@@ -402,9 +404,9 @@ module AEPrinter = struct
     | L_built BVULE -> Fmt.pf ppf "<="
     | L_neg_built BVULE -> Fmt.pf ppf ">"
     | L_built (IsConstr h) ->
-      Fmt.pf ppf "? %a" Uid.pp h
+      Fmt.pf ppf "? %a" DE.Term.Const.print h
     | L_neg_built (IsConstr h) ->
-      Fmt.pf ppf "?not? %a" Uid.pp h
+      Fmt.pf ppf "?not? %a" DE.Term.Const.print h
 
   let pp_form ppf f =
     match f with
@@ -488,7 +490,8 @@ module SmtPrinter = struct
 
     (* DT theory *)
     | Record -> ()
-    | Access s | Constr s | Destruct s -> Uid.pp ppf s
+    | Access tcst | Constr tcst | Destruct tcst ->
+      DE.Term.Const.print ppf tcst
 
     (* Float theory *)
     | Float -> Fmt.pf ppf "ae.round"
diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli
index 145e72bc1..eb93fb3e7 100644
--- a/src/lib/structures/symbols.mli
+++ b/src/lib/structures/symbols.mli
@@ -27,7 +27,7 @@
 
 type builtin =
     LE | LT (* arithmetic *)
-  | IsConstr of Uid.term_cst (* ADT tester *)
+  | IsConstr of Dolmen.Std.Expr.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type operator =
@@ -35,9 +35,9 @@ type operator =
   (* Arithmetic *)
   | Plus | Minus | Mult | Div | Modulo | Pow
   (* ADTs *)
-  | Access of Uid.term_cst | Record
-  | Constr of Uid.term_cst (* enums, adts *)
-  | Destruct of Uid.term_cst
+  | Access of Dolmen.Std.Expr.term_cst | Record
+  | Constr of Dolmen.Std.Expr.term_cst (* enums, adts *)
+  | Destruct of Dolmen.Std.Expr.term_cst
   (* Arrays *)
   | Get | Set
   (* BV *)
@@ -180,8 +180,8 @@ val var : Var.t -> t
 val int : string -> t
 val bitv : string -> t
 val real : string -> t
-val constr : Uid.term_cst -> t
-val destruct : Uid.term_cst -> t
+val constr : Dolmen.Std.Expr.term_cst -> t
+val destruct : Dolmen.Std.Expr.term_cst -> t
 val mk_bound : bound_kind -> Ty.t -> is_open:bool -> is_lower:bool -> bound
 val mk_in : bound -> bound -> t
 val mk_maps_to : Var.t -> t
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 16740982f..31716e50a 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -25,24 +25,26 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module DE = Dolmen.Std.Expr
+
 type t =
   | Tint
   | Treal
   | Tbool
   | Tvar of tvar
   | Tbitv of int
-  | Text of t list * Uid.ty_cst
+  | Text of t list * DE.ty_cst
   | Tfarray of t * t
-  | Tadt of Uid.ty_cst * t list
+  | Tadt of DE.ty_cst * t list
   | Trecord of trecord
 
 and tvar = { v : int ; mutable value : t option }
 
 and trecord = {
   mutable args : t list;
-  name : Uid.ty_cst;
-  mutable lbs :  (Uid.term_cst * t) list;
-  record_constr : Uid.term_cst;
+  name : DE.ty_cst;
+  mutable lbs :  (DE.term_cst * t) list;
+  record_constr : DE.term_cst;
   (* for ADTs that become records. default is "{" *)
 }
 
@@ -55,10 +57,11 @@ module Smtlib = struct
     | Tfarray (a_t, r_t) ->
       Fmt.pf ppf "(Array %a %a)" pp a_t pp r_t
     | Text ([], name)
-    | Trecord { args = []; name; _ } | Tadt (name, []) -> Uid.pp ppf name
+    | Trecord { args = []; name; _ } | Tadt (name, []) ->
+      DE.Ty.Const.print ppf name
     | Text (args, name)
     | Trecord { args; name; _ } | Tadt (name, args) ->
-      Fmt.(pf ppf "(@[%a %a@])" Uid.pp name (list ~sep:sp pp) args)
+      Fmt.(pf ppf "(@[%a %a@])" DE.Ty.Const.print name (list ~sep:sp pp) args)
     | Tvar { v; value = None; _ } -> Fmt.pf ppf "A%d" v
     | Tvar { value = Some t; _ } -> pp ppf t
 end
@@ -69,8 +72,8 @@ exception TypeClash of t*t
 exception Shorten of t
 
 type adt_constr =
-  { constr : Uid.term_cst ;
-    destrs : (Uid.term_cst * t) list }
+  { constr : DE.term_cst ;
+    destrs : (DE.term_cst * t) list }
 
 type type_body = adt_constr list
 
@@ -79,7 +82,7 @@ let assoc_destrs hs cases =
   try
     List.iter
       (fun {constr = s ; destrs = t} ->
-         if Uid.equal hs s then begin
+         if DE.Term.Const.equal hs s then begin
            res := Some t;
            raise Exit
          end
@@ -104,7 +107,7 @@ let print_generic body_of =
       | Tvar{v=v ; value = None} -> fprintf fmt "'a_%d" v
       | Tvar{v=v ; value = Some (Trecord { args = l; name = n; _ } as t) } ->
         if Hashtbl.mem h v then
-          fprintf fmt "%a %a" print_list l Uid.pp n
+          fprintf fmt "%a %a" print_list l DE.Ty.Const.print n
         else
           (Hashtbl.add h v ();
            (*fprintf fmt "('a_%d->%a)" v print t *)
@@ -113,28 +116,28 @@ let print_generic body_of =
         (*fprintf fmt "('a_%d->%a)" v print t *)
         print body_of fmt t
       | Text(l, s) when l == [] ->
-        fprintf fmt "<ext>%a" Uid.pp s
+        fprintf fmt "<ext>%a" DE.Ty.Const.print s
       | Text(l,s) ->
-        fprintf fmt "%a <ext>%a" print_list l Uid.pp s
+        fprintf fmt "%a <ext>%a" print_list l DE.Ty.Const.print s
       | Tfarray (t1, t2) ->
         fprintf fmt "(%a,%a) farray" (print body_of) t1 (print body_of) t2
       | Trecord { args = lv; name = n; lbs = lbls; _ } ->
         begin
-          fprintf fmt "%a <record>%a" print_list lv Uid.pp n;
+          fprintf fmt "%a <record>%a" print_list lv DE.Ty.Const.print n;
           if body_of != None then begin
             fprintf fmt " = {";
             let first = ref true in
             List.iter
               (fun (s, t) ->
                  fprintf fmt "%s%a : %a" (if !first then "" else "; ")
-                   Uid.pp s (print body_of) t;
+                   DE.Term.Const.print s (print body_of) t;
                  first := false
               ) lbls;
             fprintf fmt "}"
           end
         end
       | Tadt (n, lv) ->
-        fprintf fmt "%a <adt>%a" print_list lv Uid.pp n;
+        fprintf fmt "%a <adt>%a" print_list lv DE.Ty.Const.print n;
         begin match body_of with
           | None -> ()
           | Some type_body ->
@@ -144,7 +147,7 @@ let print_generic body_of =
             List.iter
               (fun {constr = s ; destrs = t} ->
                  fprintf fmt "%s%a%a" (if !first then "" else " | ")
-                   Uid.pp s print_adt_tuple t;
+                   DE.Term.Const.print s print_adt_tuple t;
                  first := false
               ) cases;
             fprintf fmt "}"
@@ -153,10 +156,10 @@ let print_generic body_of =
   and print_adt_tuple fmt = function
     | [] -> ()
     | (d, e)::l ->
-      Format.fprintf fmt " of { %a : %a " Uid.pp d (print None) e;
+      Format.fprintf fmt " of { %a : %a " DE.Term.Const.print d (print None) e;
       List.iter
         (fun (d, e) ->
-           Format.fprintf fmt "; %a : %a " Uid.pp d (print None) e
+           Format.fprintf fmt "; %a : %a " DE.Term.Const.print d (print None) e
         ) l;
       Format.fprintf fmt "}"
 
@@ -231,7 +234,7 @@ let rec compare t1 t2 =
   | Tvar{ v = v1; _ } , Tvar{ v = v2; _ } -> Int.compare v1 v2
   | Tvar _, _ -> -1 | _ , Tvar _ -> 1
   | Text(l1, s1) , Text(l2, s2) ->
-    let c = Uid.compare s1 s2 in
+    let c = DE.Ty.Const.compare s1 s2 in
     if c<>0 then c
     else compare_list l1 l2
   | Text _, _ -> -1 | _ , Text _ -> 1
@@ -242,7 +245,7 @@ let rec compare t1 t2 =
   | Tfarray _, _ -> -1 | _ , Tfarray _ -> 1
   | Trecord { args = a1; name = s1; lbs = l1; _ },
     Trecord { args = a2; name = s2; lbs = l2; _ } ->
-    let c = Uid.compare s1 s2 in
+    let c = DE.Ty.Const.compare s1 s2 in
     if c <> 0 then c else
       let c = compare_list a1 a2 in
       if c <> 0 then c else
@@ -251,7 +254,7 @@ let rec compare t1 t2 =
   | Trecord _, _ -> -1 | _ , Trecord _ -> 1
 
   | Tadt (s1, pars1), Tadt (s2, pars2) ->
-    let c = Uid.compare s1 s2 in
+    let c = DE.Ty.Const.compare s1 s2 in
     if c <> 0 then c
     else compare_list pars1 pars2
   (* no need to compare bodies *)
@@ -282,7 +285,7 @@ let rec equal t1 t2 =
   match shorten t1 , shorten t2 with
   | Tvar{ v = v1; _ }, Tvar{ v = v2; _ } -> v1 = v2
   | Text(l1, s1), Text(l2, s2) ->
-    (try Uid.equal s1 s2 && List.for_all2 equal l1 l2
+    (try DE.Ty.Const.equal s1 s2 && List.for_all2 equal l1 l2
      with Invalid_argument _ -> false)
   | Tfarray (ta1, ta2), Tfarray (tb1, tb2) ->
     equal ta1 tb1 && equal ta2 tb2
@@ -290,10 +293,10 @@ let rec equal t1 t2 =
     Trecord { args = a2; name = s2; lbs = l2; _ } ->
     begin
       try
-        Uid.equal s1 s2 && List.for_all2 equal a1 a2 &&
+        DE.Ty.Const.equal s1 s2 && List.for_all2 equal a1 a2 &&
         List.for_all2
           (fun (l1, ty1) (l2, ty2) ->
-             Uid.equal l1 l2 && equal ty1 ty2) l1 l2
+             DE.Term.Const.equal l1 l2 && equal ty1 ty2) l1 l2
       with Invalid_argument _ -> false
     end
   | Tint, Tint | Treal, Treal | Tbool, Tbool -> true
@@ -301,7 +304,7 @@ let rec equal t1 t2 =
 
   | Tadt (s1, pars1), Tadt (s2, pars2) ->
     begin
-      try Uid.equal s1 s2 && List.for_all2 equal pars1 pars2
+      try DE.Ty.Const.equal s1 s2 && List.for_all2 equal pars1 pars2
       with Invalid_argument _ -> false
       (* no need to compare bodies *)
     end
@@ -320,17 +323,17 @@ let rec matching s pat t =
     (try if not (equal (M.find n s) t) then raise (TypeClash(pat,t)); s
      with Not_found -> M.add n t s)
   | Tvar { value = _; _ }, _ -> raise (Shorten pat)
-  | Text (l1,s1) , Text (l2,s2) when Uid.equal s1 s2 ->
+  | Text (l1,s1) , Text (l2,s2) when DE.Ty.Const.equal s1 s2 ->
     List.fold_left2 matching s l1 l2
   | Tfarray (ta1,ta2), Tfarray (tb1,tb2) ->
     matching (matching s ta1 tb1) ta2 tb2
-  | Trecord r1, Trecord r2 when Uid.equal r1.name r2.name ->
+  | Trecord r1, Trecord r2 when DE.Ty.Const.equal r1.name r2.name ->
     let s = List.fold_left2 matching s r1.args r2.args in
     List.fold_left2
       (fun s (_, p) (_, ty) -> matching s p ty) s r1.lbs r2.lbs
   | Tint , Tint | Tbool , Tbool | Treal , Treal -> s
   | Tbitv n , Tbitv m when n=m -> s
-  | Tadt(n1, args1), Tadt(n2, args2) when Uid.equal n1 n2 ->
+  | Tadt(n1, args1), Tadt(n2, args2) when DE.Ty.Const.equal n1 n2 ->
     List.fold_left2 matching s args1 args2
   | _ , _ ->
     raise (TypeClash(pat,t))
@@ -418,7 +421,7 @@ let fresh_list lty subst = fresh_list (List.map shorten lty) subst
 
 module Decls = struct
 
-  module MH = Uid.Ty_map
+  module MH = Map.Make (DE.Ty.Const)
 
   module MTY = Map.Make(struct
       type ty = t
@@ -501,7 +504,7 @@ module Decls = struct
         add name params cases;
         cases
     with Not_found ->
-      Printer.print_err "%a not found" Uid.pp name;
+      Printer.print_err "%a not found" DE.Ty.Const.print name;
       assert false
 
   let reinit () = decls := MH.empty
@@ -523,7 +526,7 @@ let fresh_empty_text =
       let path = DStd.Path.global @@ Fmt.str "'_c%d" !cpt in
       DStd.Expr.Ty.Const.mk path 0
     in
-    text [] (Uid.of_ty_cst id)
+    text [] id
 
 let t_adt ?(body=None) s ty_vars =
   let ty = Tadt (s, ty_vars) in
@@ -546,49 +549,36 @@ let t_adt ?(body=None) s ty_vars =
   end;
   ty
 
-module DE = Dolmen.Std.Expr
-
 let tunit =
   let () =
     match Dolmen.Std.Expr.Ty.definition DE.Ty.Const.unit with
     | Some def -> Nest.attach_orders [def]
     | None -> assert false
   in
-  let void = Uid.of_term_cst DE.Term.Cstr.void in
-  let body = Some [void, []] in
-  let ty = t_adt ~body (Uid.of_ty_cst DE.Ty.Const.unit) [] in
+  let body = Some [DE.Term.Cstr.void, []] in
+  let ty = t_adt ~body DE.Ty.Const.unit [] in
   ty
 
-let trecord ?(sort_fields = false) ~record_constr lv name lbs =
-  let lbs =
-    if sort_fields then
-      List.sort (fun (l1, _) (l2, _) -> Uid.compare l1 l2) lbs
-    else
-      lbs
-  in
+let trecord ~record_constr lv name lbs =
   Trecord { record_constr; args = lv; name; lbs = lbs}
 
 let rec hash t =
   match t with
   | Tvar{ v; _ } -> v
   | Text(l,s) ->
-    abs (List.fold_left (fun acc x-> acc*19 + hash x) (Uid.hash s) l)
+    abs (List.fold_left (fun acc x-> acc*19 + hash x) (DE.Ty.Const.hash s) l)
   | Tfarray (t1,t2) -> 19 * (hash t1) + 23 * (hash t2)
-  | Trecord { args; name = s; lbs; _ } ->
-    let h =
-      List.fold_left (fun h ty -> 27 * h + hash ty) (Uid.hash s) args
-    in
+  | Trecord { args; name = s; _ } ->
+    (* We do not hash constructors. *)
     let h =
-      List.fold_left
-        (fun h (lb, ty) -> 23 * h + 19 * (Uid.hash lb) + hash ty)
-        (abs h) lbs
+      List.fold_left (fun h ty -> 27 * h + hash ty) (DE.Ty.Const.hash s) args
     in
     abs h
 
-  | Tadt (s, args) ->
+  | Tadt (ty, args) ->
     (* We do not hash constructors. *)
     let h =
-      List.fold_left (fun h ty -> 31 * h + hash ty) (Uid.hash s) args
+      List.fold_left (fun h ty -> 31 * h + hash ty) (DE.Ty.Const.hash ty) args
     in
     abs h
 
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 9b0a72db3..dbd03cd4a 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -42,7 +42,7 @@ type t =
   (** Type variables *)
   | Tbitv of int
   (** Bitvectors of a given length *)
-  | Text of t list * Uid.ty_cst
+  | Text of t list * Dolmen.Std.Expr.ty_cst
   (** Abstract types applied to arguments. [Text (args, s)] is
       the application of the abstract type constructor [s] to
       arguments [args]. *)
@@ -51,7 +51,7 @@ type t =
   (** Functional arrays. [TFarray (src,dst)] maps values of type [src]
       to values of type [dst]. *)
 
-  | Tadt of Uid.ty_cst * t list
+  | Tadt of Dolmen.Std.Expr.ty_cst * t list
   (** Application of algebraic data types. [Tadt (a, params)] denotes
       the application of the polymorphic datatype [a] to the types parameters
       [params].
@@ -77,22 +77,22 @@ and tvar = {
 and trecord = {
   mutable args : t list;
   (** Arguments passed to the record constructor *)
-  name : Uid.ty_cst;
+  name : Dolmen.Std.Expr.ty_cst;
   (** Name of the record type *)
-  mutable lbs :  (Uid.term_cst * t) list;
+  mutable lbs :  (Dolmen.Std.Expr.term_cst * t) list;
   (** List of fields of the record. Each field has a name,
       and an associated type. *)
-  record_constr : Uid.term_cst;
+  record_constr : Dolmen.Std.Expr.term_cst;
   (** record constructor. Useful is case it's a specialization of an
       algeberaic datatype. Default value is "\{__[name]" *)
 }
 (** Record types. *)
 
 type adt_constr =
-  { constr : Uid.term_cst ;
+  { constr : Dolmen.Std.Expr.term_cst ;
     (** constructor of an ADT type *)
 
-    destrs : (Uid.term_cst * t) list
+    destrs : (Dolmen.Std.Expr.term_cst * t) list
     (** the list of destructors associated with the constructor and
         their respective types *)
   }
@@ -109,12 +109,12 @@ module Set : Set.S with type elt = t
 (** Sets of types *)
 
 
-val assoc_destrs : Uid.term_cst -> adt_constr list -> (Uid.term_cst * t) list
+val assoc_destrs : Dolmen.Std.Expr.term_cst -> adt_constr list -> (Dolmen.Std.Expr.term_cst * t) list
 (** [assoc_destrs cons cases] returns the list of destructors associated with
     the constructor [cons] in the ADT defined by [cases].
     @raises Not_found if the constructor is not in the given list. *)
 
-val type_body : Uid.ty_cst -> t list -> type_body
+val type_body : Dolmen.Std.Expr.ty_cst -> t list -> type_body
 
 (** {2 Type inspection} *)
 
@@ -160,13 +160,13 @@ val fresh_tvar : unit -> t
 val fresh_empty_text : unit -> t
 (** Return a fesh abstract type. *)
 
-val text : t list -> Uid.ty_cst -> t
+val text : t list -> Dolmen.Std.Expr.ty_cst -> t
 (** Apply the abstract type constructor to the list of type arguments
     given. *)
 
 val t_adt :
-  ?body:((Uid.term_cst * (Uid.term_cst * t) list) list) option ->
-  Uid.ty_cst -> t list -> t
+  ?body:((Dolmen.Std.Expr.term_cst * (Dolmen.Std.Expr.term_cst * t) list) list) option ->
+  Dolmen.Std.Expr.ty_cst -> t list -> t
 (** Create an algebraic datatype. The body is a list of
     constructors, where each constructor is associated with the list of
     its destructors with their respective types. If [body] is none,
@@ -175,9 +175,8 @@ val t_adt :
     of arguments. *)
 
 val trecord :
-  ?sort_fields:bool ->
-  record_constr:Uid.term_cst ->
-  t list -> Uid.ty_cst -> (Uid.term_cst * t) list -> t
+  record_constr:Dolmen.Std.Expr.term_cst ->
+  t list -> Dolmen.Std.Expr.ty_cst -> (Dolmen.Std.Expr.term_cst * t) list -> t
 (** Create a record type. [trecord args name lbs] creates a record
     type with name [name], arguments [args] and fields [lbs].
 
diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml
index eb2dc0381..168e7c8a0 100644
--- a/src/lib/structures/typed.ml
+++ b/src/lib/structures/typed.ml
@@ -27,6 +27,8 @@
 
 (** Anotations (used by the GUI). *)
 
+module DE = Dolmen.Std.Expr
+
 type ('a, 'b) annoted =
   { c : 'a;
     annot : 'b }
@@ -52,7 +54,7 @@ type oplogic =
 
 (** type of pattern in match construct of ADTs *)
 type pattern =
-  | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list}
+  | Constr of { name : DE.term_cst ; args : (Var.t * DE.term_cst * Ty.t) list}
   (** A pattern case which is a constructor. [name] is the name of
       constructor. [args] contains the variables bound by this pattern
       with their correponsing destructors and types *)
@@ -264,7 +266,7 @@ let rec print_term =
         (fun (p, v) ->
            match p with
            | Constr {name = n; args = l} ->
-             fprintf fmt "| %a %a -> %a\n" Uid.pp n pp_vars l
+             fprintf fmt "| %a %a -> %a\n" DE.Term.Const.print n pp_vars l
                print_term v
            | Var x ->
              fprintf fmt "| %a -> %a\n" Var.print x print_term v;
diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli
index 525e2712f..f23992689 100644
--- a/src/lib/structures/typed.mli
+++ b/src/lib/structures/typed.mli
@@ -72,7 +72,10 @@ type oplogic =
 (** Logic operators. *)
 
 type pattern =
-  | Constr of { name : Uid.term_cst ; args : (Var.t * Uid.term_cst * Ty.t) list}
+  | Constr of {
+      name : Dolmen.Std.Expr.term_cst ;
+      args : (Var.t * Dolmen.Std.Expr.term_cst * Ty.t) list
+    }
   | Var of Var.t
 
 
diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml
deleted file mode 100644
index 2d352db0e..000000000
--- a/src/lib/structures/uid.ml
+++ /dev/null
@@ -1,102 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) 2022-2024 --- OCamlPro SAS                           *)
-(*                                                                        *)
-(*     This file is distributed under the terms of OCamlPro               *)
-(*     Non-Commercial Purpose License, version 1.                         *)
-(*                                                                        *)
-(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
-(*     use this file under the terms of the Apache Software License       *)
-(*     version 2.0.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-module DStd = Dolmen.Std
-module DE = Dolmen.Std.Expr
-
-type _ t =
-  | Term_cst : DE.term_cst -> DE.term_cst t
-  | Ty_cst : DE.ty_cst -> DE.ty_cst t
-  | Ty_var : DE.ty_var -> DE.ty_var t
-
-type term_cst = DE.term_cst t
-type ty_cst = DE.ty_cst t
-type ty_var = DE.ty_var t
-
-let order_tag : int DStd.Tag.t = DStd.Tag.create ()
-
-let has_order_if_constr id =
-  let is_constr DE.{ builtin; _ } =
-    match builtin with
-    | DStd.Builtin.Constructor _ -> true
-    | _ -> false
-  in
-  let has_attached_order id =
-    DE.Term.Const.get_tag id order_tag |> Option.is_some
-  in
-  (not (is_constr id)) || has_attached_order id
-
-let[@inline always] of_term_cst id =
-  (* This assertion ensures that the API of the [Nest] module have been
-     correctly used, that is [Nest.attach_orders] have been called on
-     the nest of [id] if [id] is a constructor of ADT. *)
-  if not @@ has_order_if_constr id then
-    Fmt.invalid_arg "no order on %a" DE.Id.print id;
-  Term_cst id
-
-let[@inline always] of_ty_cst id = Ty_cst id
-let[@inline always] of_ty_var id = Ty_var id
-
-let hash (type a) (u : a t) =
-  match u with
-  | Term_cst id -> DE.Id.hash id
-  | Ty_cst id -> DE.Id.hash id
-  | Ty_var id -> DE.Id.hash id
-
-let pp (type a) ppf (u : a t) =
-  match u with
-  | Term_cst id -> DE.Id.print ppf id
-  | Ty_cst id -> DE.Id.print ppf id
-  | Ty_var id -> DE.Id.print ppf id
-
-let show (type a) (u : a t) = Fmt.to_to_string pp u
-
-let equal (type a b) (u1 : a t) (u2 : b t) =
-  match u1, u2 with
-  | Term_cst id1, Term_cst id2 -> DE.Id.equal id1 id2
-  | Ty_cst id1, Ty_cst id2 -> DE.Id.equal id1 id2
-  | Ty_var id1, Ty_var id2 -> DE.Id.equal id1 id2
-  | _ -> String.equal (show u1) (show u2)
-
-let compare (type a b) (u1 : a t) (u2 : b t) =
-  match u1, u2 with
-  | Term_cst id1, Term_cst id2 -> DE.Id.compare id1 id2
-  | Ty_cst id1, Ty_cst id2 -> DE.Id.compare id1 id2
-  | Ty_var id1, Ty_var id2 -> DE.Id.compare id1 id2
-  | _ -> String.compare (show u1) (show u2)
-
-module Term_set = Set.Make
-    (struct
-      type nonrec t = term_cst
-      let compare = compare
-    end)
-
-module Ty_map = Map.Make
-    (struct
-      type nonrec t = ty_cst
-      let compare = compare
-    end)
diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli
deleted file mode 100644
index 501e8b88d..000000000
--- a/src/lib/structures/uid.mli
+++ /dev/null
@@ -1,53 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     Alt-Ergo: The SMT Solver For Software Verification                 *)
-(*     Copyright (C) --- OCamlPro SAS                                     *)
-(*                                                                        *)
-(*     This file is distributed under the terms of OCamlPro               *)
-(*     Non-Commercial Purpose License, version 1.                         *)
-(*                                                                        *)
-(*     As an exception, Alt-Ergo Club members at the Gold level can       *)
-(*     use this file under the terms of the Apache Software License       *)
-(*     version 2.0.                                                       *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     The Alt-Ergo theorem prover                                        *)
-(*                                                                        *)
-(*     Sylvain Conchon, Evelyne Contejean, Francois Bobot                 *)
-(*     Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout              *)
-(*                                                                        *)
-(*     CNRS - INRIA - Universite Paris Sud                                *)
-(*                                                                        *)
-(*     ---------------------------------------------------------------    *)
-(*                                                                        *)
-(*     More details can be found in the directory licenses/               *)
-(*                                                                        *)
-(**************************************************************************)
-
-module DE = Dolmen.Std.Expr
-
-type _ t = private
-  | Term_cst : DE.term_cst -> DE.term_cst t
-  | Ty_cst : DE.ty_cst -> DE.ty_cst t
-  | Ty_var : DE.ty_var -> DE.ty_var t
-
-type term_cst = DE.term_cst t
-type ty_cst = DE.ty_cst t
-type ty_var = DE.ty_var t
-
-val of_term_cst : DE.term_cst -> term_cst
-val of_ty_cst : DE.ty_cst -> ty_cst
-val of_ty_var : DE.ty_var -> ty_var
-
-val hash : 'a t -> int
-val pp : 'a t Fmt.t
-val show : 'a t -> string
-val equal : 'a t -> 'a t -> bool
-val compare : 'a t -> 'a t -> int
-
-val order_tag : int Dolmen.Std.Tag.t
-(** Tag used to attach the order of constructor. *)
-
-module Term_set : Set.S with type elt = term_cst
-module Ty_map : Map.S with type key = ty_cst
diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml
index b11106e4e..b108422c2 100644
--- a/src/lib/structures/xliteral.ml
+++ b/src/lib/structures/xliteral.ml
@@ -25,9 +25,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
+module DE = Dolmen.Std.Expr
+
 type builtin = Symbols.builtin =
     LE | LT | (* arithmetic *)
-    IsConstr of Uid.term_cst (* ADT tester *)
+    IsConstr of DE.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type 'a view =
@@ -126,9 +128,9 @@ let print_view ?(lbl="") pr_elt fmt vw =
   | Builtin (_, BVULE, _) ->
     assert false (* not reachable *)
 
-  | Builtin (pos, IsConstr hs, [e]) ->
+  | Builtin (pos, IsConstr tcst, [e]) ->
     Format.fprintf fmt "%s(%a ? %a)"
-      (if pos then "" else "not ") pr_elt e Uid.pp hs
+      (if pos then "" else "not ") pr_elt e DE.Term.Const.print tcst
 
   | Builtin (_, IsConstr _, _) ->
     assert false (* not reachable *)
@@ -193,7 +195,7 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
   let equal_builtins n1 n2 =
     match n1, n2 with
     | LT, LT | LE, LE -> true
-    | IsConstr h1, IsConstr h2 -> Uid.equal h1 h2
+    | IsConstr tcst1, IsConstr tcst2 -> DE.Term.Const.equal tcst1 tcst2
     | _ -> false
 
   module V = struct
diff --git a/src/lib/structures/xliteral.mli b/src/lib/structures/xliteral.mli
index 4abdbd29b..8e7afe376 100644
--- a/src/lib/structures/xliteral.mli
+++ b/src/lib/structures/xliteral.mli
@@ -27,7 +27,7 @@
 
 type builtin = Symbols.builtin =
     LE | LT | (* arithmetic *)
-    IsConstr of Uid.term_cst (* ADT tester *)
+    IsConstr of Dolmen.Std.Expr.term_cst (* ADT tester *)
   | BVULE (* unsigned bit-vector arithmetic *)
 
 type 'a view = (*private*)
diff --git a/src/lib/util/nest.ml b/src/lib/util/nest.ml
index 6a75ecd24..6b84e2ce0 100644
--- a/src/lib/util/nest.ml
+++ b/src/lib/util/nest.ml
@@ -153,6 +153,8 @@ let ty_cst_of_constr DE.{ builtin; _ } =
   | B.Constructor { adt; _ } -> adt
   | _ -> Fmt.failwith "expect an ADT constructor"
 
+let order_tag : int DStd.Tag.t = DStd.Tag.create ()
+
 let attach_orders defs =
   let hp = build_graph defs in
   let r : (int * DE.term_cst list) H.t = H.create 17 in
@@ -162,7 +164,7 @@ let attach_orders defs =
     let { id; outgoing; in_degree;  _ } = Hp.pop_min hp in
     let ty = ty_cst_of_constr id in
     let o = H.add_constr r ty id in
-    DE.Term.Const.set_tag id Uid.order_tag o;
+    DE.Term.Const.set_tag id order_tag o;
     assert (in_degree = 0);
     List.iter
       (fun node ->
@@ -175,14 +177,13 @@ let attach_orders defs =
   done
 
 let perfect_hash id =
-  match (id : _ Uid.t) with
-  | Term_cst ({ builtin = B.Constructor _; _ } as id) ->
-    begin match DE.Term.Const.get_tag id Uid.order_tag with
+  match (id : DE.term_cst) with
+  | { builtin = B.Constructor _; _ } as id ->
+    begin match DE.Term.Const.get_tag id order_tag with
       | Some h -> h
       | None ->
         (* Cannot occur as we eliminate this case in the smart constructor
            [Uid.of_term_cst]. *)
         assert false
     end
-  | Term_cst _ -> invalid_arg "Nest.perfect_hash"
-  | _ -> .
+  | _ -> invalid_arg "Nest.perfect_hash"
diff --git a/src/lib/util/nest.mli b/src/lib/util/nest.mli
index d8b30d862..c9e8ca74b 100644
--- a/src/lib/util/nest.mli
+++ b/src/lib/util/nest.mli
@@ -36,7 +36,7 @@ val attach_orders : DE.ty_def list -> unit
     (in any order). By nest, we mean the set of all the constructors in a
     mutually recursive definition of ADTs. *)
 
-val perfect_hash : Uid.term_cst -> int
+val perfect_hash : Dolmen.Std.Expr.term_cst -> int
 (** [perfect_hash u] returns an integer between [0] and [n] exclusive where
     [u] is a constructor and [n] is the number of constructors of the ADT of
     [u].