diff --git a/charon-ml/src/GAstOfJson.ml b/charon-ml/src/GAstOfJson.ml
index 66fbbe7f..0c116ccb 100644
--- a/charon-ml/src/GAstOfJson.ml
+++ b/charon-ml/src/GAstOfJson.ml
@@ -215,7 +215,7 @@ let big_int_of_json (js : json) : (big_int, string) result =
     | `String is -> Ok (Z.of_string is)
     | _ -> Error "")
 
-(** Deserialize a {!scalar_value} from JSON and **check the ranges**.
+(** Deserialize a {!Values.scalar_value} from JSON and **check the ranges**.
 
     Note that in practice we also check that the values are in range
     in the interpreter functions. Still, it doesn't cost much to be
diff --git a/charon-ml/src/NameMatcher.ml b/charon-ml/src/NameMatcher.ml
index a9bd9d94..00a1b278 100644
--- a/charon-ml/src/NameMatcher.ml
+++ b/charon-ml/src/NameMatcher.ml
@@ -14,22 +14,22 @@
       writing patterns by hand)
 
     Here are some examples of patterns:
-    - "core::mem::replace": the function `core::mem::replace`
-    - "alloc::vec::{alloc::vec::Vec<@>}::push": the function `push` in any
-      impl block of type `alloc::vec::Vec<T>`, where T is a type variable.
-      Note that "@" means that this matches any (type) variable. In case
+    - ["core::mem::replace"]: the function [core::mem::replace]
+    - ["alloc::vec::{alloc::vec::Vec<@>}::push"]: the function [push] in any
+      impl block of type [alloc::vec::Vec<T>], where T is a type variable.
+      Note that ["@"] means that this matches any (type) variable. In case
       we need stronger constraints, we can name those variables: "@T". All the
-      occurrences of "@T" must match the same variable (ex.: "Foo<@T, @T>"
-      would match `Foo<U, U>` but not `Foo<T, U>`).
-    - the "@" syntax is used both for types and const generics. For regions/lifetimes,
-      we use "'": "&'a mut @T"
+      occurrences of  ["@T"] must match the same variable (ex.: ["Foo<@T, @T>"]
+      would match [Foo<U, U>] but not [Foo<T, U>]).
+    - the ["@"] syntax is used both for types and const generics. For regions/lifetimes,
+      we use ["'"]: ["&'a mut @T"]
     - for the types we put inside blocks, we have syntax for arrays, slices,
       and references:
-      - "[@T; @N]": slice
-      - "&'R mut @T": mutable reference
+      - ["[@T; @N]"]: slice
+      - ["&'R mut @T"]: mutable reference
 
-    Remark: `Box` is treated as a primitive type, which means that one only
-    needs to type "Box" (instead of "alloc::boxed::Box" - though the latter
+    Remark: [Box] is treated as a primitive type, which means that one only
+    needs to type ["Box"] (instead of ["alloc::boxed::Box"] - though the latter
     also works).
  *)
 
@@ -66,11 +66,11 @@ type match_config = {
       (** If true, only allow matching variables to variables.
 
           This is important when matching names: if the pattern
-          is `alloc::boxed::{Box<@T>}::new`, we only want to match
-          names where `@T` is a variable. For instance, we wouldn't
-          want to match `alloc::boxed::{Box<u32>}::new` (if it existed...).
+          is [alloc::boxed::{Box<@T>}::new], we only want to match
+          names where [@T] is a variable. For instance, we wouldn't
+          want to match [alloc::boxed::{Box<u32>}::new] (if it existed...).
           However, we might want to match instantiations (i.e., for which
-          `@T` is matched to `usize`) when matching function calls inside
+          [@T] is matched to [usize]) when matching function calls inside
           bodies.
        *)
 }
diff --git a/charon-ml/src/Types.ml b/charon-ml/src/Types.ml
index c8c37a76..b5e74983 100644
--- a/charon-ml/src/Types.ml
+++ b/charon-ml/src/Types.ml
@@ -15,7 +15,7 @@ module RegionGroupId = IdGen ()
 module Disambiguator = IdGen ()
 
 (** We define this type to control the name of the visitor functions
-    (see e.g., {!Types.iter_ty_base} and {!Types.TypeVar}).
+    (see e.g., {!class:Types.iter_ty_base} and {!Types.TVar}).
   *)
 type type_var_id = TypeVarId.id [@@deriving show, ord]
 
diff --git a/charon-ml/src/TypesUtils.ml b/charon-ml/src/TypesUtils.ml
index 8a209314..e49a2d96 100644
--- a/charon-ml/src/TypesUtils.ml
+++ b/charon-ml/src/TypesUtils.ml
@@ -46,7 +46,7 @@ let type_decl_get_fields (def : type_decl)
 let type_decl_is_enum (def : type_decl) : bool =
   match def.kind with Struct _ -> false | Enum _ -> true | Opaque -> false
 
-(** Return [true] if a {!type: Types.ty} is actually [unit] *)
+(** Return [true] if a {!type:Charon.Types.ty} is actually [unit] *)
 let ty_is_unit (ty : ty) : bool =
   match ty with
   | TAdt
@@ -185,7 +185,7 @@ let ty_regions_intersect (ty : ty) (regions : RegionId.Set.t) : bool =
   let ty_regions = ty_regions ty in
   not (RegionId.Set.disjoint ty_regions regions)
 
-(** Check if a {!type: Types.ty} contains regions from a given set *)
+(** Check if a {!type:Charon.Types.ty} contains regions from a given set *)
 let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : ty) : bool =
   let obj =
     object