Update the code documentation to fix links and syntax issues

41 files changed, 1263 insertions, 1256 deletions

diff --git a/Makefile b/Makefile
index 3b822802..eb09d1a0 100644
--- a/Makefile
+++ b/Makefile
@@ -31,7 +31,7 @@ build-tests-verify: build tests verify
 
 # Build the project
 .PHONY: build
-build: build-driver build-lib
+build: build-driver build-lib doc
 
 .PHONY: build-driver
 build-driver:
diff --git a/src/Assumed.ml b/src/Assumed.ml
index 1e8bb669..cb089c08 100644
--- a/src/Assumed.ml
+++ b/src/Assumed.ml
@@ -1,32 +1,32 @@
 (** This module contains various utilities for the assumed functions.
 
-    Note that `Box::free` is peculiar: we don't really handle it as a function,
-    because it is legal to free a box whose boxed value is `⊥` (it often
+    Note that [Box::free] is peculiar: we don't really handle it as a function,
+    because it is legal to free a box whose boxed value is [⊥] (it often
     happens that we move a value out of a box before freeing this box).
-    Semantically speaking, we thus handle `Box::free` as a value drop and
+    Semantically speaking, we thus handle [Box::free] as a value drop and
     not as a function call, and thus never need its signature.
     
     TODO: implementing the concrete evaluation functions for the assumed
     functions is really annoying (see
     [InterpreterStatements.eval_non_local_function_call_concrete]).
     I think it should be possible, in most situations, to write bodies which
-    model the behaviour of those unsafe functions. For instance, `Box::deref_mut`
+    model the behaviour of those unsafe functions. For instance, [Box::deref_mut]
     should simply be:
-    ```
-    fn deref_mut<'a, T>(x : &'a mut Box<T>) -> &'a mut T {
-      &mut ( *x ) // box dereferencement is a primitive operation
-    }
-    ```
+    {[
+      fn deref_mut<'a, T>(x : &'a mut Box<T>) -> &'a mut T {
+        &mut ( *x ) // box dereferencement is a primitive operation
+      }
+    ]}
     
     For vectors, we could "cheat" by using the index as a field index (vectors
     would be encoded as ADTs with a variable number of fields). Of course, it
     would require a bit of engineering, but it would probably be quite lightweight
     in the end.
-    ```
-    Vec::get_mut<'a,T>(v : &'a mut Vec<T>, i : usize) -> &'a mut T {
-      &mut ( ( *x ).i )
-    }
-    ```
+    {[
+      Vec::get_mut<'a,T>(v : &'a mut Vec<T>, i : usize) -> &'a mut T {
+        &mut ( ( *x ).i )
+      }
+    ]}
  *)
 
 open Names
@@ -46,11 +46,11 @@ module Sig = struct
   (** Region 'a of id 0 *)
   let region_param_0 : T.region_var = { T.index = rvar_id_0; name = Some "'a" }
 
-  (** Region group: { parent={}; regions:{'a of id 0} } *)
+  (** Region group: [{ parent={}; regions:{'a of id 0} }] *)
   let region_group_0 : T.region_var_group =
     { T.id = rg_id_0; regions = [ rvar_id_0 ]; parents = [] }
 
-  (** Type parameter `T` of id 0 *)
+  (** Type parameter [T] of id 0 *)
   let type_param_0 : T.type_var = { T.index = tvar_id_0; name = "T" }
 
   let mk_ref_ty (r : T.RegionVarId.id T.region) (ty : T.sty) (is_mut : bool) :
@@ -58,7 +58,7 @@ module Sig = struct
     let ref_kind = if is_mut then T.Mut else T.Shared in
     mk_ref_ty r ty ref_kind
 
-  (** `fn<T>(&'a mut T, T) -> T` *)
+  (** [fn<T>(&'a mut T, T) -> T] *)
   let mem_replace_sig : A.fun_sig =
     (* The signature fields *)
     let region_params = [ region_param_0 ] (* <'a> *) in
@@ -77,7 +77,7 @@ module Sig = struct
       output;
     }
 
-  (** `fn<T>(T) -> Box<T>` *)
+  (** [fn<T>(T) -> Box<T>] *)
   let box_new_sig : A.fun_sig =
     {
       region_params = [];
@@ -88,7 +88,7 @@ module Sig = struct
       output = mk_box_ty tvar_0 (* Box<T> *);
     }
 
-  (** `fn<T>(Box<T>) -> ()` *)
+  (** [fn<T>(Box<T>) -> ()] *)
   let box_free_sig : A.fun_sig =
     {
       region_params = [];
@@ -99,9 +99,9 @@ module Sig = struct
       output = mk_unit_ty (* () *);
     }
 
-  (** Helper for `Box::deref_shared` and `Box::deref_mut`.
+  (** Helper for [Box::deref_shared] and [Box::deref_mut].
       Returns:
-      `fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T`
+      [fn<'a, T>(&'a (mut) Box<T>) -> &'a (mut) T]
   *)
   let box_deref_gen_sig (is_mut : bool) : A.fun_sig =
     (* The signature fields *)
@@ -117,13 +117,13 @@ module Sig = struct
       output = mk_ref_ty rvar_0 tvar_0 is_mut (* &'a (mut) T *);
     }
 
-  (** `fn<'a, T>(&'a Box<T>) -> &'a T` *)
+  (** [fn<'a, T>(&'a Box<T>) -> &'a T] *)
   let box_deref_shared_sig = box_deref_gen_sig false
 
-  (** `fn<'a, T>(&'a mut Box<T>) -> &'a mut T` *)
+  (** [fn<'a, T>(&'a mut Box<T>) -> &'a mut T] *)
   let box_deref_mut_sig = box_deref_gen_sig true
 
-  (** `fn<T>() -> Vec<T>` *)
+  (** [fn<T>() -> Vec<T>] *)
   let vec_new_sig : A.fun_sig =
     let region_params = [] in
     let regions_hierarchy = [] in
@@ -139,7 +139,7 @@ module Sig = struct
       output;
     }
 
-  (** `fn<T>(&'a mut Vec<T>, T)` *)
+  (** [fn<T>(&'a mut Vec<T>, T)] *)
   let vec_push_sig : A.fun_sig =
     (* The signature fields *)
     let region_params = [ region_param_0 ] in
@@ -161,7 +161,7 @@ module Sig = struct
       output;
     }
 
-  (** `fn<T>(&'a mut Vec<T>, usize, T)` *)
+  (** [fn<T>(&'a mut Vec<T>, usize, T)] *)
   let vec_insert_sig : A.fun_sig =
     (* The signature fields *)
     let region_params = [ region_param_0 ] in
@@ -184,7 +184,7 @@ module Sig = struct
       output;
     }
 
-  (** `fn<T>(&'a Vec<T>) -> usize` *)
+  (** [fn<T>(&'a Vec<T>) -> usize] *)
   let vec_len_sig : A.fun_sig =
     (* The signature fields *)
     let region_params = [ region_param_0 ] in
@@ -204,7 +204,7 @@ module Sig = struct
     }
 
   (** Helper:
-      `fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T`
+      [fn<T>(&'a (mut) Vec<T>, usize) -> &'a (mut) T]
    *)
   let vec_index_gen_sig (is_mut : bool) : A.fun_sig =
     (* The signature fields *)
@@ -227,10 +227,10 @@ module Sig = struct
       output;
     }
 
-  (** `fn<T>(&'a Vec<T>, usize) -> &'a T` *)
+  (** [fn<T>(&'a Vec<T>, usize) -> &'a T] *)
   let vec_index_shared_sig : A.fun_sig = vec_index_gen_sig false
 
-  (** `fn<T>(&'a mut Vec<T>, usize) -> &'a mut T` *)
+  (** [fn<T>(&'a mut Vec<T>, usize) -> &'a mut T] *)
   let vec_index_mut_sig : A.fun_sig = vec_index_gen_sig true
 end
 
@@ -241,11 +241,11 @@ type assumed_info = A.assumed_fun_id * A.fun_sig * bool * name
     - a boolean indicating whether the function can fail or not
     - their name
 
-    Rk.: following what is written above, we don't include `Box::free`.
+    Rk.: following what is written above, we don't include [Box::free].
     
-    Remark about the vector functions: for `Vec::len` to be correct and return
-    a `usize`, we have to make sure that vectors are bounded by the max usize.
-    Followingly, `Vec::push` is monadic.
+    Remark about the vector functions: for [Vec::len] to be correct and return
+    a [usize], we have to make sure that vectors are bounded by the max usize.
+    Followingly, [Vec::push] is monadic.
  *)
 let assumed_infos : assumed_info list =
   let deref_pre = [ "core"; "ops"; "deref" ] in
diff --git a/src/Collections.ml b/src/Collections.ml
index 351b6523..0933b3e4 100644
--- a/src/Collections.ml
+++ b/src/Collections.ml
@@ -7,10 +7,10 @@ module List = struct
 
   (** Split a list at a given index.
   
-      `split_at ls i` splits `ls` into two lists where the first list has
-      length `i`.
+      [split_at ls i] splits [ls] into two lists where the first list has
+      length [i].
       
-      Raise `Failure` if the list is too short.
+      Raise [Failure] if the list is too short.
   *)
   let rec split_at (ls : 'a list) (i : int) =
     if i < 0 then raise (Invalid_argument "split_at take positive integers")
@@ -26,7 +26,7 @@ module List = struct
 
   (** Pop the last element of a list
      
-      Raise `Failure` if the list is empty.
+      Raise [Failure] if the list is empty.
    *)
   let rec pop_last (ls : 'a list) : 'a list * 'a =
     match ls with
@@ -58,7 +58,7 @@ module List = struct
 
   (** Fold and link the iterations.
 
-      Similar to [iter_link] but for fold left operations.
+      Similar to {!iter_link} but for fold left operations.
    *)
   let fold_left_link (link : unit -> unit) (f : 'a -> 'b -> 'a) (init : 'a)
       (ls : 'b list) : 'a =
@@ -107,15 +107,15 @@ module type Map = sig
   val add_list : (key * 'a) list -> 'a t -> 'a t
   val of_list : (key * 'a) list -> 'a t
 
-  val to_string : string option -> ('a -> string) -> 'a t -> string
   (** "Simple" pretty printing function.
   
       Is useful when we need to customize a bit [show_t], but without using
       something as burdensome as [pp_t].
   
-      `to_string (Some indent) m` prints `m` by breaking line after every binding
-      and inserting `indent`.
+      [to_string (Some indent) m] prints [m] by breaking line after every binding
+      and inserting [indent].
    *)
+  val to_string : string option -> ('a -> string) -> 'a t -> string
 
   val pp : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
   val show : ('a -> string) -> 'a t -> string
@@ -172,15 +172,15 @@ module type Set = sig
   val add_list : elt list -> t -> t
   val of_list : elt list -> t
 
-  val to_string : string option -> t -> string
   (** "Simple" pretty printing function.
   
       Is useful when we need to customize a bit [show_t], but without using
       something as burdensome as [pp_t].
   
-      `to_string (Some indent) s` prints `s` by breaking line after every element
-      and inserting `indent`.
+      [to_string (Some indent) s] prints [s] by breaking line after every element
+      and inserting [indent].
    *)
+  val to_string : string option -> t -> string
 
   val pp : Format.formatter -> t -> unit
   val show : t -> string
@@ -283,7 +283,7 @@ module type InjMap = sig
   val of_list : (key * elem) list -> t
 end
 
-(** See [InjMap] *)
+(** See {!InjMap} *)
 module MakeInjMap (Key : OrderedType) (Elem : OrderedType) :
   InjMap with type key = Key.t with type elem = Elem.t = struct
   module Map = MakeMap (Key)
diff --git a/src/Contexts.ml b/src/Contexts.ml
index 07535e06..510976f4 100644
--- a/src/Contexts.ml
+++ b/src/Contexts.ml
@@ -5,56 +5,56 @@ module V = Values
 open ValuesUtils
 
 (** Some global counters.
- *
- * Note that those counters were initially stored in [eval_ctx] values,
- * but it proved better to make them global and stateful:
- * - when branching (and thus executing on several paths with different
- *   contexts) it is better to really have unique ids everywhere (and
- *   not have fresh ids shared by several contexts even though introduced
- *   after the branching) because at some point we might need to merge the
- *   different contexts
- * - also, it is a lot more convenient to not store those counters in contexts
- *   objects
- *
- * =============
- * **WARNING**:
- * =============
- * Pay attention when playing with closures, as you may not always generate
- * fresh identifiers without noticing it, especially when using type abbreviations.
- * For instance, consider the following:
- * ```
- * type fun_type = unit -> ...
- * fn f x : fun_type =
- *   let id = fresh_id () in
- *   ...
- *
- * let g = f x in   // <-- the fresh identifier gets generated here
- * let x1 = g () in // <-- no fresh generation here
- * let x2 = g () in
- * ...
- * ```
- *
- * This is why, in such cases, we often introduce all the inputs, even
- * when they are not used (which happens!).
- * ```
- * fn f x : fun_type =
- *  fun .. ->
- *   let id = fresh_id () in
- *   ...
- * ```
- *
- * Note that in practice, we never reuse closures, except when evaluating
- * a branching in the execution (which is fine, because the branches evaluate
- * independentely of each other). Still, it is always a good idea to be
- * defensive.
- *
- * However, the same problem arises with logging. 
- *
- * Also, a more defensive way would be to not use global references, and
- * store the counters in the evaluation context. This is actually what was
- * originally done, before we updated the code to use global counters because
- * it proved more convenient (and even before updating the code of the
- * interpreter to use CPS).
+
+  Note that those counters were initially stored in {!eval_ctx} values,
+  but it proved better to make them global and stateful:
+  - when branching (and thus executing on several paths with different
+    contexts) it is better to really have unique ids everywhere (and
+    not have fresh ids shared by several contexts even though introduced
+    after the branching) because at some point we might need to merge the
+    different contexts
+  - also, it is a lot more convenient to not store those counters in contexts
+    objects
+
+  =============
+  **WARNING**:
+  =============
+  Pay attention when playing with closures, as you may not always generate
+  fresh identifiers without noticing it, especially when using type abbreviations.
+  For instance, consider the following:
+  {[
+    type fun_type = unit -> ...
+    fn f x : fun_type =
+      let id = fresh_id () in
+      ...
+   
+    let g = f x in   // <-- the fresh identifier gets generated here
+    let x1 = g () in // <-- no fresh generation here
+    let x2 = g () in
+    ...
+  ]}
+
+  This is why, in such cases, we often introduce all the inputs, even
+  when they are not used (which happens!).
+  {[
+    fn f x : fun_type =
+     fun .. ->
+      let id = fresh_id () in
+      ...
+  ]}
+
+  Note that in practice, we never reuse closures, except when evaluating
+  a branching in the execution (which is fine, because the branches evaluate
+  independentely of each other). Still, it is always a good idea to be
+  defensive.
+
+  However, the same problem arises with logging. 
+
+  Also, a more defensive way would be to not use global references, and
+  store the counters in the evaluation context. This is actually what was
+  originally done, before we updated the code to use global counters because
+  it proved more convenient (and even before updating the code of the
+  interpreter to use CPS).
  *)
 
 let symbolic_value_id_counter, fresh_symbolic_value_id =
@@ -87,12 +87,12 @@ let reset_global_counters () =
   abstraction_id_counter := AbstractionId.generator_zero;
   fun_call_id_counter := FunCallId.generator_zero
 
+(** A binder used in an environment, to map a variable to a value *)
 type binder = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;  (** Possible name *)
 }
 [@@deriving show]
-(** A binder used in an environment, to map a variable to a value *)
 
 (** Environment value: mapping from variable to value, abstraction (only
     used in symbolic mode) or stack frame delimiter.
@@ -113,7 +113,7 @@ type env_elem =
         name = "iter_env_elem";
         variety = "iter";
         ancestors = [ "iter_abs" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -121,7 +121,7 @@ type env_elem =
         name = "map_env_elem";
         variety = "map";
         ancestors = [ "map_abs" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
 
@@ -133,7 +133,7 @@ type env = env_elem list
         name = "iter_env";
         variety = "iter";
         ancestors = [ "iter_env_elem" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -141,7 +141,7 @@ type env = env_elem list
         name = "map_env";
         variety = "map";
         ancestors = [ "map_env_elem" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
 
@@ -189,13 +189,13 @@ type config = {
 }
 [@@deriving show]
 
+(** See {!config} *)
 type partial_config = {
   check_invariants : bool;
   greedy_expand_symbolics_with_borrows : bool;
   allow_bottom_below_borrow : bool;
   return_unit_end_abs_with_no_loans : bool;
 }
-(** See [config] *)
 
 let config_of_partial (mode : interpreter_mode) (config : partial_config) :
     config =
@@ -220,6 +220,7 @@ type fun_context = { fun_decls : fun_decl FunDeclId.Map.t } [@@deriving show]
 type global_context = { global_decls : global_decl GlobalDeclId.Map.t }
 [@@deriving show]
 
+(** Evaluation context *)
 type eval_ctx = {
   type_context : type_context;
   fun_context : fun_context;
@@ -229,7 +230,6 @@ type eval_ctx = {
   ended_regions : RegionId.Set.t;
 }
 [@@deriving show]
-(** Evaluation context *)
 
 let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var =
   TypeVarId.nth ctx.type_vars vid
@@ -366,11 +366,11 @@ let ctx_read_first_dummy_var (ctx : eval_ctx) : typed_value =
   in
   read_var ctx.env
 
-(** Push an uninitialized variable (which thus maps to [Bottom]) *)
+(** Push an uninitialized variable (which thus maps to {!Values.Bottom}) *)
 let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
   ctx_push_var ctx var (mk_bottom var.var_ty)
 
-(** Push a list of uninitialized variables (which thus map to [Bottom]) *)
+(** Push a list of uninitialized variables (which thus map to {!Values.Bottom}) *)
 let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom v.var_ty)) vars in
   ctx_push_vars ctx vars
diff --git a/src/Cps.ml b/src/Cps.ml
index 2d7dd2be..c2c0363b 100644
--- a/src/Cps.ml
+++ b/src/Cps.ml
@@ -22,25 +22,25 @@ type sexpr = SOne | SList of sexpr list
 
 type eval_result = SA.expression option
 
-type m_fun = C.eval_ctx -> eval_result
 (** Continuation function *)
+type m_fun = C.eval_ctx -> eval_result
 
-type cm_fun = m_fun -> m_fun
 (** Continuation taking another continuation as parameter *)
+type cm_fun = m_fun -> m_fun
 
-type typed_value_m_fun = V.typed_value -> m_fun
 (** Continuation taking a typed value as parameter - TODO: use more *)
+type typed_value_m_fun = V.typed_value -> m_fun
 
-type typed_value_cm_fun = V.typed_value -> cm_fun
 (** Continuation taking another continuation as parameter and a typed
     value as parameter.
  *)
+type typed_value_cm_fun = V.typed_value -> cm_fun
 
-type st_m_fun = statement_eval_res -> m_fun
 (** Type of a continuation used when evaluating a statement *)
+type st_m_fun = statement_eval_res -> m_fun
 
-type st_cm_fun = st_m_fun -> m_fun
 (** Type of a continuation used when evaluating a statement *)
+type st_cm_fun = st_m_fun -> m_fun
 
 (** Convert a unit function to a cm function *)
 let unit_to_cm_fun (f : C.eval_ctx -> unit) : cm_fun =
@@ -65,9 +65,9 @@ let comp_unit (f : cm_fun) (g : C.eval_ctx -> unit) : cm_fun =
 let comp_update (f : cm_fun) (g : C.eval_ctx -> C.eval_ctx) : cm_fun =
   comp f (update_to_cm_fun g)
 
-(** This is just a test, to check that [comp] is general enough to handle a case
+(** This is just a test, to check that {!comp} is general enough to handle a case
     where a function must compute a value and give it to the continuation.
-    It happens for functions like [eval_operand].
+    It happens for functions like {!InterpreterExpressions.eval_operand}.
 
     Keeping this here also makes it a good reference, when one wants to figure
     out the signatures he should use for such a composition.
@@ -79,8 +79,8 @@ let comp_ret_val (f : (V.typed_value -> m_fun) -> m_fun)
 let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx
 let id_cm_fun : cm_fun = fun cf ctx -> cf ctx
 
-(** If we have a list of [inputs] of type `'a list` and a function [f] which
-    evaluates one element of type `'a` to compute a result of type `'b` before
+(** If we have a list of [inputs] of type ['a list] and a function [f] which
+    evaluates one element of type ['a] to compute a result of type ['b] before
     giving it to a continuation, the following function performs a fold operation:
     it evaluates all the inputs one by one by accumulating the results in a list,
     and gives the list to a continuation.
@@ -101,7 +101,7 @@ let fold_left_apply_continuation (f : 'a -> ('c -> 'd) -> 'c -> 'd)
   in
   eval_list inputs cf
 
-(** Unit test/example for [fold_left_apply_continuation] *)
+(** Unit test/example for {!fold_left_apply_continuation} *)
 let _ =
   fold_left_apply_continuation
     (fun x cf (ctx : int) -> cf (ctx + x))
@@ -109,8 +109,8 @@ let _ =
     (fun (ctx : int) -> assert (ctx = 4321))
     0
 
-(** If we have a list of [inputs] of type `'a list` and a function [f] which
-    evaluates one element of type `'a` to compute a result of type `'b` before
+(** If we have a list of [inputs] of type ['a list] and a function [f] which
+    evaluates one element of type ['a] to compute a result of type ['b] before
     giving it to a continuation, the following function performs a fold operation:
     it evaluates all the inputs one by one by accumulating the results in a list,
     and gives the list to a continuation.
@@ -133,7 +133,7 @@ let fold_left_list_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd)
   in
   eval_list inputs cf []
 
-(** Unit test/example for [fold_left_list_apply_continuation] *)
+(** Unit test/example for {!fold_left_list_apply_continuation} *)
 let _ =
   fold_left_list_apply_continuation
     (fun x cf (ctx : unit) -> cf (10 + x) ctx)
@@ -144,23 +144,23 @@ let _ =
 (** Composition of functions taking continuations as parameters.
 
     We sometimes have the following situation, where we want to compose three
-    functions `send`, `transmit` and `receive` such that:
+    functions [send], [transmit] and [receive] such that:
     - those three functions take continuations as parameters
-    - `send` generates a value and gives it to its continuation
-    - `receive` expects a value (so we can compose `send` and `receive` like
-      so: `comp send receive`)
-    - `transmit` doesn't expect any value and needs to be called between `send`
-      and `receive`
+    - [send] generates a value and gives it to its continuation
+    - [receive] expects a value (so we can compose [send] and [receive] like
+      so: [comp send receive])
+    - [transmit] doesn't expect any value and needs to be called between [send]
+      and [receive]
     
-    In this situation, we need to take the value given by `send` and "transmit"
-    it to `receive`.
+    In this situation, we need to take the value given by [send] and "transmit"
+    it to [receive].
 
     This is what this function does (see the unit test below for an illustration).
  *)
 let comp_transmit (f : ('v -> 'm) -> 'n) (g : 'm -> 'm) : ('v -> 'm) -> 'n =
  fun cf -> f (fun v -> g (cf v))
 
-(** Example of use of [comp_transmit] *)
+(** Example of use of {!comp_transmit} *)
 let () =
   let return3 (cf : int -> unit -> unit) (ctx : unit) = cf 3 ctx in
   let do_nothing (cf : unit -> unit) (ctx : unit) = cf ctx in
@@ -182,7 +182,7 @@ let comp_check_value (f : ('v -> 'ctx -> 'a) -> 'ctx -> 'b)
       g v ctx;
       cf v ctx)
 
-(** This case is similar to [comp_check_value], but even simpler (we only check
+(** This case is similar to {!comp_check_value}, but even simpler (we only check
     the context)
  *)
 let comp_check_ctx (f : ('ctx -> 'a) -> 'ctx -> 'b) (g : 'ctx -> unit) :
diff --git a/src/Expressions.ml b/src/Expressions.ml
index bf06dd1e..e2eaf1e7 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -82,21 +82,21 @@ type operand =
 
     Note that ADTs are desaggregated at some point in MIR. For instance, if
     we have in Rust:
-    ```
-    let ls = Cons(hd, tl);
-    ```
+    {[
+      let ls = Cons(hd, tl);
+    ]}
     
     In MIR we have (yes, the discriminant update happens *at the end* for some
     reason):
-    ```
-    (ls as Cons).0 = move hd;
-    (ls as Cons).1 = move tl;
-    discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
-    ```
+    {[
+      (ls as Cons).0 = move hd;
+      (ls as Cons).1 = move tl;
+      discriminant(ls) = 0; // assuming [Cons] is the variant of index 0
+    ]}
     
     Note that in our semantics, we handle both cases (in case of desaggregated
-    initialization, `ls` is initialized to `⊥`, then this `⊥` is expanded to
-    `Cons (⊥, ⊥)` upon the first assignment, at which point we can initialize
+    initialization, [ls] is initialized to [⊥], then this [⊥] is expanded to
+    [Cons (⊥, ⊥)] upon the first assignment, at which point we can initialize
     the field 0, etc.).
  *)
 type aggregate_kind =
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index b537e181..5d212941 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -10,19 +10,19 @@ module F = Format
 
 (** A qualifier for a type definition.
 
-    Controls whether we should use `type ...` or `and ...` (for mutually
+    Controls whether we should use [type ...] or [and ...] (for mutually
     recursive datatypes).
  *)
 type type_decl_qualif =
-  | Type  (** `type t = ...` *)
-  | And  (** `type t0 = ... and t1 = ...` *)
-  | AssumeType  (** `assume type t` *)
-  | TypeVal  (** In an fsti: `val t : Type0` *)
+  | Type  (** [type t = ...] *)
+  | And  (** [type t0 = ... and t1 = ...] *)
+  | AssumeType  (** [assume type t] *)
+  | TypeVal  (** In an fsti: [val t : Type0] *)
 
 (** A qualifier for function definitions.
 
-    Controls whether we should use `let ...`, `let rec ...` or `and ...`,
-    or only generate a declaration with `val` or `assume val`
+    Controls whether we should use [let ...], [let rec ...] or [and ...],
+    or only generate a declaration with [val] or [assume val]
  *)
 type fun_decl_qualif = Let | LetRec | And | Val | AssumeVal
 
@@ -59,7 +59,7 @@ let fstar_unop_name (unop : unop) : string =
 
 (** Small helper to compute the name of a binary operation (note that many
     binary operations like "less than" are extracted to primitive operations,
-    like `<`.
+    like [<].
  *)
 let fstar_named_binop_name (binop : E.binop) (int_ty : integer_type) : string =
   let binop =
@@ -213,40 +213,40 @@ let fstar_extract_binop (extract_expr : bool -> texpression -> unit)
   if inside then F.pp_print_string fmt ")"
 
 (**
- * [ctx]: we use the context to lookup type definitions, to retrieve type names.
- * This is used to compute variable names, when they have no basenames: in this
- * case we use the first letter of the type name.
- *
- * [variant_concatenate_type_name]: if true, add the type name as a prefix
- * to the variant names.
- * Ex.:
- * In Rust:
- *   ```
- *   enum List = {
- *     Cons(u32, Box<List>),x
- *     Nil,
- *   }
- *   ```
- *
- * F*, if option activated:
- *   ```
- *   type list =
- *   | ListCons : u32 -> list -> list
- *   | ListNil : list
- *   ```
- *
- * F*, if option not activated:
- *   ```
- *   type list =
- *   | Cons : u32 -> list -> list
- *   | Nil : list
- *   ```
- *
- * Rk.: this should be true by default, because in Rust all the variant names
- * are actively uniquely identifier by the type name `List::Cons(...)`, while
- * in other languages it is not necessarily the case, and thus clashes can mess
- * up type checking. Note that some languages actually forbids the name clashes
- * (it is the case of F* ).
+   [ctx]: we use the context to lookup type definitions, to retrieve type names.
+   This is used to compute variable names, when they have no basenames: in this
+   case we use the first letter of the type name.
+  
+   [variant_concatenate_type_name]: if true, add the type name as a prefix
+   to the variant names.
+   Ex.:
+   In Rust:
+     {[
+       enum List = {
+         Cons(u32, Box<List>),x
+         Nil,
+       }
+     ]}
+  
+   F*, if option activated:
+     {[
+       type list =
+       | ListCons : u32 -> list -> list
+       | ListNil : list
+     ]}
+  
+   F*, if option not activated:
+     {[
+       type list =
+       | Cons : u32 -> list -> list
+       | Nil : list
+     ]}
+  
+   Rk.: this should be true by default, because in Rust all the variant names
+   are actively uniquely identifier by the type name [List::Cons(...)], while
+   in other languages it is not necessarily the case, and thus clashes can mess
+   up type checking. Note that some languages actually forbids the name clashes
+   (it is the case of F* ).
  *)
 let mk_formatter (ctx : trans_ctx) (crate_name : string)
     (variant_concatenate_type_name : bool) : formatter =
@@ -430,7 +430,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   }
 
 (** [inside] constrols whether we should add parentheses or not around type
-    application (if `true` we add parentheses).
+    application (if [true] we add parentheses).
  *)
 let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
     (ty : ty) : unit =
@@ -438,8 +438,8 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   | Adt (type_id, tys) -> (
       match type_id with
       | Tuple ->
-          (* This is a bit annoying, but in F* `()` is not the unit type:
-           * we have to write `unit`... *)
+          (* This is a bit annoying, but in F* [()] is not the unit type:
+           * we have to write [unit]... *)
           if tys = [] then F.pp_print_string fmt "unit"
           else (
             F.pp_print_string fmt "(";
@@ -513,31 +513,31 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
 let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
     (def : type_decl) (fields : field list) : unit =
   (* We want to generate a definition which looks like this:
-   * ```
-   * type t = { x : int; y : bool; }
-   * ```
-   *
-   * If there isn't enough space on one line:
-   * ```
-   * type t =
-   * {
-   *   x : int; y : bool;
-   * }
-   * ```
-   * 
-   * And if there is even less space:
-   * ```
-   * type t =
-   * {
-   *   x : int;
-   *   y : bool;
-   * }
-   * ```
-   *
-   * Also, in case there are no fields, we need to define the type as `unit`
-   * (`type t = {}` doesn't work in F* ).
-   *)
-  (* Note that we already printed: `type t =` *)
+     {[
+       type t = { x : int; y : bool; }
+     ]}
+
+     If there isn't enough space on one line:
+     {[
+       type t =
+       {
+         x : int; y : bool;
+       }
+     ]}
+
+     And if there is even less space:
+     {[
+       type t =
+       {
+         x : int;
+         y : bool;
+       }
+     ]}
+
+     Also, in case there are no fields, we need to define the type as [unit]
+     ([type t = {}] doesn't work in F* ).
+  *)
+  (* Note that we already printed: [type t =] *)
   if fields = [] then (
     F.pp_print_space fmt ();
     F.pp_print_string fmt "unit")
@@ -572,44 +572,44 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
     (def : type_decl) (def_name : string) (type_params : string list)
     (variants : variant list) : unit =
   (* We want to generate a definition which looks like this:
-   * ```
-   * type list a = | Cons : a -> list a -> list a | Nil : list a
-   * ```
-   *
-   * If there isn't enough space on one line:
-   * ```
-   * type s =
-   * | Cons : a -> list a -> list a
-   * | Nil : list a
-   * ```
-   *
-   * And if we need to write the type of a variant on several lines:
-   * ```
-   * type s =
-   * | Cons :
-   *   a ->
-   *   list a ->
-   *   list a
-   * | Nil : list a
-   * ```
-   *
-   * Finally, it is possible to give names to the variant fields in Rust.
-   * In this situation, we generate a definition like this:
-   * ```
-   * type s =
-   * | Cons : hd:a -> tl:list a -> list a
-   * | Nil : list a
-   * ```
-   *
-   * Note that we already printed: `type s =`
-   *)
+     {[
+       type list a = | Cons : a -> list a -> list a | Nil : list a
+     ]}
+
+     If there isn't enough space on one line:
+     {[
+       type s =
+       | Cons : a -> list a -> list a
+       | Nil : list a
+     ]}
+
+     And if we need to write the type of a variant on several lines:
+     {[
+       type s =
+       | Cons :
+         a ->
+         list a ->
+         list a
+       | Nil : list a
+     ]}
+
+     Finally, it is possible to give names to the variant fields in Rust.
+     In this situation, we generate a definition like this:
+     {[
+       type s =
+       | Cons : hd:a -> tl:list a -> list a
+       | Nil : list a
+     ]}
+
+     Note that we already printed: [type s =]
+  *)
   (* Print the variants *)
   let print_variant (variant_id : VariantId.id) (variant : variant) : unit =
     let variant_name = ctx_get_variant (AdtId def.def_id) variant_id ctx in
     F.pp_print_space fmt ();
     F.pp_open_hvbox fmt ctx.indent_incr;
     (* variant box *)
-    (* `| Cons :`
+    (* [| Cons :]
      * Note that we really don't want any break above so we print everything
      * at once. *)
     F.pp_print_string fmt ("| " ^ variant_name ^ " :");
@@ -619,7 +619,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
       (* Open the field box *)
       F.pp_open_box fmt ctx.indent_incr;
       (* Print the field names
-       * `  x :`
+       * [  x :]
        * Note that when printing fields, we register the field names as
        * *variables*: they don't need to be unique at the top level. *)
       let ctx =
@@ -638,7 +638,7 @@ let extract_type_decl_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
       in
       (* Print the field type *)
       extract_ty ctx fmt false f.field_ty;
-      (* Print the arrow `->`*)
+      (* Print the arrow [->]*)
       F.pp_print_space fmt ();
       F.pp_print_string fmt "->";
       (* Close the field box *)
@@ -749,7 +749,7 @@ let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
   F.pp_open_hvbox fmt 0;
   (* Retrieve the name *)
   let state_name = ctx_get_assumed_type State ctx in
-  (* The qualif should be `AssumeType` or `TypeVal` *)
+  (* The qualif should be [AssumeType] or [TypeVal] *)
   (match qualif with
   | Type | And -> raise (Failure "Unexpected")
   | AssumeType ->
@@ -830,9 +830,9 @@ let extract_adt_g_value
       ctx
   | Adt (adt_id, _) ->
       (* "Regular" ADT *)
-      (* We print something of the form: `Cons field0 ... fieldn`.
+      (* We print something of the form: [Cons field0 ... fieldn].
        * We could update the code to print something of the form:
-       * `{ field0=...; ...; fieldn=...; }` in case of structures.
+       * [{ field0=...; ...; fieldn=...; }] in case of structures.
        *)
       let cons =
         match variant_id with
@@ -888,10 +888,10 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter)
     TODO: replace the formatting boolean [inside] with something more general?
     Also, it seems we don't really use it...
     Cases to consider:
-    - right-expression in a let: `let x = re in _` (never parentheses?)
-    - next expression in a let:  `let x = _ in next_e` (never parentheses?)
-    - application argument: `f (exp)`
-    - match/if scrutinee: `if exp then _ else _`/`match exp | _ -> _`
+    - right-expression in a let: [let x = re in _] (never parentheses?)
+    - next expression in a let:  [let x = _ in next_e] (never parentheses?)
+    - application argument: [f (exp)]
+    - match/if scrutinee: [if exp then _ else _]/[match exp | _ -> _]
  *)
 let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (e : texpression) : unit =
@@ -1019,9 +1019,9 @@ and extract_adt_cons (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       F.pp_print_string fmt ")"
   | _ ->
       (* "Regular" ADT *)
-      (* We print something of the form: `Cons field0 ... fieldn`.
+      (* We print something of the form: [Cons field0 ... fieldn].
        * We could update the code to print something of the form:
-       * `{ field0=...; ...; fieldn=...; }` in case of fully
+       * [{ field0=...; ...; fieldn=...; }] in case of fully
        * applied structure constructors.
        *)
       let cons =
@@ -1044,7 +1044,7 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
     (inside : bool) (original_app : texpression) (proj : projection)
     (_proj_type_params : ty list) (args : texpression list) : unit =
   (* We isolate the first argument (if there is), in order to pretty print the
-   * projection (`x.field` instead of `MkAdt?.field x` *)
+   * projection ([x.field] instead of [MkAdt?.field x] *)
   match args with
   | [ arg ] ->
       (* Exactly one argument: pretty-print *)
@@ -1144,13 +1144,13 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
   (* Extract the switch *)
   (match body with
   | If (e_then, e_else) ->
-      (* Open a box for the `if` *)
+      (* Open a box for the [if] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
       F.pp_print_string fmt "if";
       F.pp_print_space fmt ();
       let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
-      (* Close the box for the `if` *)
+      (* Close the box for the [if] *)
       F.pp_close_box fmt ();
       (* Extract the branches *)
       let extract_branch (is_then : bool) (e_branch : texpression) : unit =
@@ -1162,14 +1162,14 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
         F.pp_print_space fmt ();
         (* Open a box for the branch *)
         F.pp_open_hovbox fmt ctx.indent_incr;
-        (* Print the `begin` if necessary *)
+        (* Print the [begin] if necessary *)
         let parenth = PureUtils.let_group_requires_parentheses e_branch in
         if parenth then (
           F.pp_print_string fmt "begin";
           F.pp_print_space fmt ());
         (* Print the branch expression *)
         extract_texpression ctx fmt false e_branch;
-        (* Close the `begin ... end ` *)
+        (* Close the [begin ... end ] *)
         if parenth then (
           F.pp_print_space fmt ();
           F.pp_print_string fmt "end");
@@ -1182,16 +1182,16 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
       extract_branch true e_then;
       extract_branch false e_else
   | Match branches ->
-      (* Open a box for the `match ... with` *)
+      (* Open a box for the [match ... with] *)
       F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Print the `match ... with` *)
+      (* Print the [match ... with] *)
       F.pp_print_string fmt "begin match";
       F.pp_print_space fmt ();
       let scrut_inside = PureUtils.let_group_requires_parentheses scrut in
       extract_texpression ctx fmt scrut_inside scrut;
       F.pp_print_space fmt ();
       F.pp_print_string fmt "with";
-      (* Close the box for the `match ... with` *)
+      (* Close the box for the [match ... with] *)
       F.pp_close_box fmt ();
 
       (* Extract the branches *)
@@ -1281,7 +1281,7 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter)
   (ctx, ctx_body)
 
 (** A small utility to print the types of the input parameters in the form:
-    `u32 -> list u32 -> ...`
+    [u32 -> list u32 -> ...]
     (we don't print the return type of the function)
     
     This is used for opaque function declarations, in particular.
@@ -1302,14 +1302,14 @@ let extract_fun_input_parameters_types (ctx : extraction_ctx)
     In order to help the user, we can generate a template for the functions
     required by the decreases clauses. We simply generate definitions of
     the following form in a separate file:
-    ```
-    let f_decrease (t : Type0) (x : t) : nat = admit()
-    ```
+    {[
+      let f_decrease (t : Type0) (x : t) : nat = admit()
+    ]}
     
-    Where the translated functions for `f` look like this:
-    ```
-    let f_fwd (t : Type0) (x : t) : Tot ... (decreases (f_decrease t x)) = ...
-    ```
+    Where the translated functions for [f] look like this:
+    {[
+      let f_fwd (t : Type0) (x : t) : Tot ... (decreases (f_decrease t x)) = ...
+    ]}
  *)
 let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
     (def : fun_decl) : unit =
@@ -1324,7 +1324,7 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter)
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
   F.pp_open_hvbox fmt 0;
-  (* Add the `unfold` keyword *)
+  (* Add the [unfold] keyword *)
   F.pp_print_string fmt "unfold";
   F.pp_print_space fmt ();
   (* Open a box for "let FUN_NAME (PARAMS) : EFFECT = admit()" *)
@@ -1410,10 +1410,10 @@ let extract_fun_decl (ctx : extraction_ctx) (fmt : F.formatter)
     F.pp_open_hovbox fmt ctx.indent_incr;
     (* Print the return type *)
     (* For opaque definitions, as we don't have named parameters under the hand,
-     * we don't print parameters in the form `(x : a) (y : b) ...` above,
-     * but wait until here to print the types: `a -> b -> ...`. *)
+     * we don't print parameters in the form [(x : a) (y : b) ...] above,
+     * but wait until here to print the types: [a -> b -> ...]. *)
     if is_opaque then extract_fun_input_parameters_types ctx fmt def;
-    (* `Tot` *)
+    (* [Tot] *)
     if has_decreases_clause then (
       F.pp_print_string fmt "Tot";
       F.pp_print_space fmt ());
@@ -1547,11 +1547,11 @@ let extract_global_decl_body (ctx : extraction_ctx) (fmt : F.formatter)
     We generate the body which computes the global value separately from the value declaration itself.
 
     For example in Rust,
-    `static X: u32 = 3;`
+    [static X: u32 = 3;]
 
     will be translated to:
-    `let x_body : result u32 = Return 3`
-    `let x_c : u32 = eval_global x_body`
+    [let x_body : result u32 = Return 3]
+    [let x_c : u32 = eval_global x_body]
  *)
 let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
     (global : A.global_decl) (body : fun_decl) (interface : bool) : unit =
@@ -1590,10 +1590,10 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
 (** Extract a unit test, if the function is a unit function (takes no
     parameters, returns unit).
     
-    A unit test simply checks that the function normalizes to `Return ()`:
-    ```
-    let _ = assert_norm (FUNCTION () = Return ())
-    ```
+    A unit test simply checks that the function normalizes to [Return ()]:
+    {[
+      let _ = assert_norm (FUNCTION () = Return ())
+    ]}
  *)
 let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
     (def : fun_decl) : unit =
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 9f6a863d..b022b18d 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -4,13 +4,13 @@ module C = Collections
     
     We often need identifiers (for definitions, variables, etc.) and in
     order to make sure we don't mix them, we use a generative functor
-    (see [IdGen]).
+    (see {!IdGen}).
 *)
 module type Id = sig
   type id
 
-  type generator
   (** Id generator - simply a counter *)
+  type generator
 
   val zero : id
   val generator_zero : generator
@@ -21,7 +21,7 @@ module type Id = sig
 
   (* TODO: this should be stateful! - but we may want to be able to duplicate
      contexts...
-     Maybe we could have a `fresh` and a `global_fresh`
+     Maybe we could have a [fresh] and a [global_fresh]
      TODO: change the order of the returned types
   *)
   val fresh : generator -> id * generator
@@ -41,19 +41,19 @@ module type Id = sig
 
   val nth_opt : 'a list -> id -> 'a option
 
-  val update_nth : 'a list -> id -> 'a -> 'a list
   (** Update the nth element of the list.
 
       Raises [Invalid_argument] if the identifier is out of range.
    *)
+  val update_nth : 'a list -> id -> 'a -> 'a list
 
   val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list
 
-  val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list
-  (** Same as [mapi], but where the indices start with 1.
+  (** Same as {!mapi}, but where the indices start with 1.
        
-      TODO: generalize to `map_from_i`
+      TODO: generalize to [map_from_i]
    *)
+  val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list
 
   val iteri : (id -> 'a -> unit) -> 'a list -> unit
 
@@ -64,7 +64,7 @@ end
 
 (** Generative functor for identifiers.
 
-    See [Id].
+    See {!Id}.
 *)
 module IdGen () : Id = struct
   (* TODO: use Z.t *)
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 9308fa16..7f51c5b9 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -44,7 +44,7 @@ let initialize_eval_context (type_context : C.type_context)
 
       Introduces local variables initialized in the following manner:
       - input arguments are initialized as symbolic values
-      - the remaining locals are initialized as ⊥
+      - the remaining locals are initialized as [⊥]
       Abstractions are introduced for the regions present in the function
       signature.
       
@@ -115,7 +115,7 @@ let initialize_symbolic_context_for_fun (type_context : C.type_context)
 (** Small helper.
 
     This is a continuation function called by the symbolic interpreter upon
-    reaching the `return` instruction when synthesizing a *backward* function:
+    reaching the [return] instruction when synthesizing a *backward* function:
     this continuation takes care of doing the proper manipulations to finish
     the synthesis (mostly by ending abstractions).
 *)
@@ -164,7 +164,7 @@ let evaluate_function_symbolic_synthesize_backward_from_return
     (* Initialize and insert the abstractions in the context.
      *
      * We take care of disallowing ending the return regions which we
-     * shouldn't end (see the documentation of the `can_end` field of [abs]
+     * shouldn't end (see the documentation of the [can_end] field of [abs]
      * for more information. *)
     let parent_and_current_rgs = T.RegionGroupId.Set.add back_id parent_rgs in
     let region_can_end rid =
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 6b920a51..30c3b221 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -16,7 +16,7 @@ let log = InterpreterBorrowsCore.log
 
 (** Auxiliary function to end borrows: lookup a borrow in the environment,
     update it (by returning an updated environment where the borrow has been
-    replaced by [Bottom])) if we can end the borrow (for instance, it is not
+    replaced by {!V.Bottom})) if we can end the borrow (for instance, it is not
     an outer borrow...) or return the reason why we couldn't update the borrow.
 
     [end_borrow] then simply performs a loop: as long as we need to end (outer)
@@ -79,6 +79,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
     object
       inherit [_] C.map_eval_ctx as super
 
+      (** We reimplement {!visit_Loan} because we may have to update the
+          outer borrows *)
       method! visit_Loan (outer : V.AbstractionId.id option * borrow_ids option)
           lc =
         match lc with
@@ -87,8 +89,6 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
             (* Update the outer borrows before diving into the shared value *)
             let outer = update_outer_borrows outer (Borrows bids) in
             V.Loan (super#visit_SharedLoan outer bids v)
-      (** We reimplement [visit_Loan] because we may have to update the
-          outer borrows *)
 
       method! visit_Borrow outer bc =
         match bc with
@@ -116,6 +116,8 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
               let outer = update_outer_borrows outer (Borrow l') in
               V.Borrow (super#visit_MutBorrow outer l' bv)
 
+      (** We reimplement {!visit_ALoan} because we may have to update the
+          outer borrows *)
       method! visit_ALoan outer lc =
         (* Note that the children avalues are just other, independent loans,
          * so we don't need to update the outer borrows when diving in.
@@ -144,8 +146,6 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
         | V.AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
             super#visit_ALoan outer lc
-      (** We reimplement [visit_ALoan] because we may have to update the
-          outer borrows *)
 
       method! visit_ABorrow outer bc =
         match bc with
@@ -169,7 +169,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
                * of the two cases described above.
                * Also note that, as we are moving the borrowed value inside the
                * abstraction (and not really giving the value back to the context)
-               * we do not insert [AEndedMutBorrow] but rather [ABottom] *)
+               * we do not insert {!AEndedMutBorrow} but rather {!ABottom} *)
               V.ABottom)
             else
               (* Update the outer borrows before diving into the child avalue *)
@@ -262,16 +262,16 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
     object (self)
       inherit [_] C.map_eval_ctx as super
 
+      (** This is a bit annoying, but as we need the type of the value we
+          are exploring, for sanity checks, we need to implement
+          {!visit_typed_avalue} instead of
+          overriding {!visit_ALoan} *)
       method! visit_typed_value opt_abs (v : V.typed_value) : V.typed_value =
         match v.V.value with
         | V.Loan lc ->
             let value = self#visit_typed_Loan opt_abs v.V.ty lc in
             ({ v with V.value } : V.typed_value)
         | _ -> super#visit_typed_value opt_abs v
-      (** This is a bit annoying, but as we need the type of the value we
-          are exploring, for sanity checks, we need to implement
-          [visit_typed_avalue] instead of
-          overriding [visit_ALoan] *)
 
       method visit_typed_Loan opt_abs ty lc =
         match lc with
@@ -295,6 +295,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               nv.V.value)
             else V.Loan (super#visit_MutLoan opt_abs bid')
 
+      (** This is a bit annoying, but as we need the type of the avalue we
+          are exploring, in order to be able to project the value we give
+          back, we need to reimplement {!visit_typed_avalue} instead of
+          {!visit_ALoan} *)
       method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
           =
         match av.V.value with
@@ -302,11 +306,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
             let value = self#visit_typed_ALoan opt_abs av.V.ty lc in
             ({ av with V.value } : V.typed_avalue)
         | _ -> super#visit_typed_avalue opt_abs av
-      (** This is a bit annoying, but as we need the type of the avalue we
-          are exploring, in order to be able to project the value we give
-          back, we need to reimplement [visit_typed_avalue] instead of
-          [visit_ALoan] *)
 
+      (** We need to inspect ignored mutable borrows, to insert loan projectors
+          if necessary.
+       *)
       method! visit_ABorrow (opt_abs : V.abs option) (bc : V.aborrow_content)
           : V.avalue =
         match bc with
@@ -339,10 +342,9 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
         | _ ->
             (* Continue exploring *)
             super#visit_ABorrow opt_abs bc
-      (** We need to inspect ignored mutable borrows, to insert loan projectors
-          if necessary.
-       *)
 
+      (** We are not specializing an already existing method, but adding a
+          new method (for projections, we need type information) *)
       method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
           (lc : V.aloan_content) : V.avalue =
         (* Preparing a bit *)
@@ -352,7 +354,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
           | Some abs -> (abs.V.regions, abs.V.ancestors_regions)
         in
         (* Rk.: there is a small issue with the types of the aloan values.
-         * See the comment at the level of definition of [typed_avalue] *)
+         * See the comment at the level of definition of {!typed_avalue} *)
         let borrowed_value_aty =
           let _, ty, _ = ty_get_ref ty in
           ty
@@ -394,7 +396,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               (* Note that we replace the ignored mut loan by an *ended* ignored
                * mut loan. Also, this is not the loan we are looking for *per se*:
                * we don't register the fact that we inserted the value somewhere
-               * (i.e., we don't call [set_replaced]) *)
+               * (i.e., we don't call {!set_replaced}) *)
               let given_back =
                 apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
                   regions ancestors_regions nv borrowed_value_aty
@@ -409,8 +411,6 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
         | V.AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
-      (** We are not specializing an already existing method, but adding a
-          new method (for projections, we need type information) *)
 
       method! visit_Abs opt_abs abs =
         (* We remember in which abstraction we are before diving -
@@ -448,26 +448,26 @@ let give_back_symbolic_value (_config : C.config)
       match nsv.sv_kind with
       | V.SynthRetGivenBack ->
           (* The given back value comes from the return value of the function
-           * we are currently synthesizing (as it is given back, it means
-           * we ended one of the regions appearing in the signature: we are
-           * currently synthesizing one of the backward functions).
-           * 
-           * As we don't allow borrow overwrites on returned value, we can
-           * (and MUST) forget the borrows *)
+             we are currently synthesizing (as it is given back, it means
+             we ended one of the regions appearing in the signature: we are
+             currently synthesizing one of the backward functions).
+
+             As we don't allow borrow overwrites on returned value, we can
+             (and MUST) forget the borrows *)
           V.AIgnoredProjBorrows
       | V.FunCallGivenBack ->
           (* TODO: there is something wrong here.
-           * Consider this:
-           * ```
-           * abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
-           * abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
-           * ```
-           *
-           * Upon ending abs1, we give back some fresh symbolic value `s1`,
-           * that we reinsert where the loan for `s0` is. However, the mutable
-           * borrow in the type `&'a mut T` was ended: we give back a value of
-           * type `T`! We thus *mustn't* introduce a projector here.
-           *)
+             Consider this:
+             {[
+               abs0 {'a} { AProjLoans (s0 : &'a mut T) [] }
+               abs1 {'b} { AProjBorrows (s0 : &'a mut T <: &'b mut T) }
+             ]}
+
+             Upon ending abs1, we give back some fresh symbolic value [s1],
+             that we reinsert where the loan for [s0] is. However, the mutable
+             borrow in the type [&'a mut T] was ended: we give back a value of
+             type [T]! We thus *mustn't* introduce a projector here.
+          *)
           V.AProjBorrows (nsv, sv.V.sv_ty)
       | _ -> failwith "Unreachable"
     in
@@ -477,7 +477,7 @@ let give_back_symbolic_value (_config : C.config)
 
 (** Auxiliary function to end borrows. See [give_back].
 
-    This function is similar to [give_back_value] but gives back an [avalue]
+    This function is similar to {!give_back_value} but gives back an {!V.avalue}
     (coming from an abstraction).
 
     It is used when ending a borrow inside an abstraction, when the corresponding
@@ -486,7 +486,7 @@ let give_back_symbolic_value (_config : C.config)
     
     REMARK: this function can't be used to give back the values borrowed by
     end abstraction when ending this abstraction. When doing this, we need
-    to convert the [avalue] to a [value] by introducing the proper symbolic values.
+    to convert the {!V.avalue} to a {!type:V.value} by introducing the proper symbolic values.
  *)
 let give_back_avalue_to_same_abstraction (_config : C.config)
     (bid : V.BorrowId.id) (mv : V.mvalue) (nv : V.typed_avalue)
@@ -501,6 +501,10 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
     object (self)
       inherit [_] C.map_eval_ctx as super
 
+      (** This is a bit annoying, but as we need the type of the avalue we
+          are exploring, in order to be able to project the value we give
+          back, we need to reimplement {!visit_typed_avalue} instead of
+          {!visit_ALoan} *)
       method! visit_typed_avalue opt_abs (av : V.typed_avalue) : V.typed_avalue
           =
         match av.V.value with
@@ -508,20 +512,18 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
             let value = self#visit_typed_ALoan opt_abs av.V.ty lc in
             ({ av with V.value } : V.typed_avalue)
         | _ -> super#visit_typed_avalue opt_abs av
-      (** This is a bit annoying, but as we need the type of the avalue we
-          are exploring, in order to be able to project the value we give
-          back, we need to reimplement [visit_typed_avalue] instead of
-          [visit_ALoan] *)
 
+      (** We are not specializing an already existing method, but adding a
+          new method (for projections, we need type information) *)
       method visit_typed_ALoan (opt_abs : V.abs option) (ty : T.rty)
           (lc : V.aloan_content) : V.avalue =
         match lc with
         | V.AMutLoan (bid', child) ->
             if bid' = bid then (
-              (* Sanity check - about why we need to call [ty_get_ref]
-               * (and don't do the same thing as in [give_back_value])
+              (* Sanity check - about why we need to call {!ty_get_ref}
+               * (and don't do the same thing as in {!give_back_value})
                * see the comment at the level of the definition of
-               * [typed_avalue] *)
+               * {!typed_avalue} *)
               let _, expected_ty, _ = ty_get_ref ty in
               if nv.V.ty <> expected_ty then (
                 log#serror
@@ -553,7 +555,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
               (* Note that we replace the ignored mut loan by an *ended* ignored
                * mut loan. Also, this is not the loan we are looking for *per se*:
                * we don't register the fact that we inserted the value somewhere
-               * (i.e., we don't call [set_replaced]) *)
+               * (i.e., we don't call {!set_replaced}) *)
               (* Sanity check *)
               assert (nv.V.ty = ty);
               V.ALoan
@@ -565,8 +567,6 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
         | V.AIgnoredSharedLoan _ ->
             (* Nothing special to do *)
             super#visit_ALoan opt_abs lc
-      (** We are not specializing an already existing method, but adding a
-          new method (for projections, we need type information) *)
     end
   in
 
@@ -690,7 +690,7 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
         else super#visit_SharedLoan env bids sv
 
       method! visit_ASharedLoan env bids v av =
-        (* This case is similar to the [SharedLoan] case *)
+        (* This case is similar to the {!SharedLoan} case *)
         if V.BorrowId.Set.mem original_bid bids then (
           set_ref ();
           let bids' = V.BorrowId.Set.add new_bid bids in
@@ -704,7 +704,7 @@ let reborrow_shared (original_bid : V.BorrowId.id) (new_bid : V.BorrowId.id)
   assert !r;
   { ctx with env }
 
-(** Auxiliary function: see [end_borrow_in_env] *)
+(** Auxiliary function: see [end_borrow] *)
 let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
     (ctx : C.eval_ctx) : C.eval_ctx =
   (* Debug *)
@@ -761,17 +761,17 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
       | V.AEndedSharedBorrow ) ->
       failwith "Unreachable"
 
-(** Convert an [avalue] to a [value].
+(** Convert an {!type:V.avalue} to a {!type:V.value}.
 
     This function is used when ending abstractions: whenever we end a borrow
-    in an abstraction, we converted the borrowed [avalue] to a fresh symbolic
-    [value], then give back this [value] to the context.
+    in an abstraction, we converted the borrowed {!V.avalue} to a fresh symbolic
+    {!type:V.value}, then give back this {!type:V.value} to the context.
  
     Note that some regions may have ended in the symbolic value we generate.
     For instance, consider the following function signature:
-    ```
-    fn f<'a>(x : &'a mut &'a mut u32);
-    ```
+    {[
+      fn f<'a>(x : &'a mut &'a mut u32);
+    ]}
     When ending the abstraction, the value given back for the outer borrow
     should be ⊥. In practice, we will give back a symbolic value which can't
     be expanded (because expanding this symbolic value would require expanding
@@ -793,11 +793,11 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
     The reason is that when ending borrows we may end abstractions, which results
     in synthesized code.
     
-    First lookup the borrow in the context and replace it with [Bottom].
+    First lookup the borrow in the context and replace it with {!V.Bottom}.
     Then, check that there is an associated loan in the context. When moving
     values, before putting the value in its destination, we get an
     intermediate state where some values are "outside" the context and thus
-    inaccessible. As [give_back_value] just performs a map for instance (TODO:
+    inaccessible. As {!give_back_value} just performs a map for instance (TODO:
     not the case anymore), we need to check independently that there is indeed a
     loan ready to receive the value we give back (note that we also have other
     invariants like: there is exacly one mutable loan associated to a mutable
@@ -808,19 +808,19 @@ let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
     Finally, give the values back.
 
     Of course, we end outer borrows before updating the target borrow if it
-    proves necessary: this is controled by the [io] parameter. If it is [Inner],
-    we allow ending inner borrows (without ending the outer borrows first),
-    otherwise we only allow ending outer borrows.
+    proves necessary.
     If a borrow is inside an abstraction, we need to end the whole abstraction,
     at the exception of the case where the loan corresponding to the borrow is
     inside the same abstraction. We control this with the [allowed_abs] parameter:
-    if it is not `None`, we allow ending a borrow if it is inside the given
-    abstraction. In practice, if the value is `Some abs_id`, we should have
+    if it is not [None], we allow ending a borrow if it is inside the given
+    abstraction. In practice, if the value is [Some abs_id], we should have
     checked that the corresponding loan is inside the abstraction given by
-    `abs_id` before. In practice, only [end_borrow] should call itself
-    with `allowed_abs = Some ...`, all the other calls should use `allowed_abs = None`:
-    if you look ath the implementation details, `end_borrow` performs
+    [abs_id] before. In practice, only {!end_borrow} should call itself
+    with [allowed_abs = Some ...], all the other calls should use [allowed_abs = None]:
+    if you look ath the implementation details, [end_borrow] performs
     all tne necessary checks in case a borrow is inside an abstraction.
+    TODO: we shouldn't allow this last case (end a borrow when the corresponding
+    loan is in the same abstraction).
     
     TODO: we should split this function in two: one function which doesn't
     perform anything smart and is trusted, and another function for the
@@ -889,7 +889,7 @@ let rec end_borrow (config : C.config) (chain : borrow_or_abs_ids)
        * borrow (if necessary) *)
       match priority with
       | OuterBorrows (Borrows bids) | InnerLoans (Borrows bids) ->
-          (* Note that we might get there with `allowed_abs <> None`: we might
+          (* Note that we might get there with [allowed_abs <> None]: we might
            * be trying to end a borrow inside an abstraction, but which is actually
            * inside another borrow *)
           let allowed_abs' = None in
@@ -1144,12 +1144,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
             ());
         super#visit_aproj env sproj
 
+      (** We may need to end borrows in "regular" values, because of shared values *)
       method! visit_borrow_content _ bc =
         match bc with
         | V.SharedBorrow (_, _) | V.MutBorrow (_, _) ->
             raise (FoundBorrowContent bc)
         | V.InactivatedMutBorrow _ -> failwith "Unreachable"
-      (** We may need to end borrows in "regular" values, because of shared values *)
     end
   in
   (* Lookup the abstraction *)
@@ -1324,30 +1324,30 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
       cf ctx
   | Some (SharedProjs projs) ->
       (* We found projectors over shared values - split between the projectors
-       * which belong to the current abstraction and the others.
-       * The context looks like this:
-       * ```
-       * abs'0 {
-       *   // The loan was initially like this:
-       *   // `shared_loan lids (s <: ...) [s]`
-       *   // but if we get there it means it was already ended:
-       *   ended_shared_loan (s <: ...) [s]
-       *   proj_shared_borrows [...; (s <: ...); ...]
-       *   proj_shared_borrows [...; (s <: ...); ...]
-       *   ...
-       * }
-       *
-       * abs'1 [
-       *   proj_shared_borrows [...; (s <: ...); ...]
-       *   ...
-       * }
-       *
-       * ...
-       *
-       * // No `s` outside of abstractions
-       * 
-       * ```
-       *)
+         which belong to the current abstraction and the others.
+         The context looks like this:
+         {[
+           abs'0 {
+             // The loan was initially like this:
+             // [shared_loan lids (s <: ...) [s]]
+             // but if we get there it means it was already ended:
+             ended_shared_loan (s <: ...) [s]
+             proj_shared_borrows [...; (s <: ...); ...]
+             proj_shared_borrows [...; (s <: ...); ...]
+             ...
+           }
+
+           abs'1 [
+             proj_shared_borrows [...; (s <: ...); ...]
+             ...
+           }
+
+           ...
+
+           // No [s] outside of abstractions
+
+         ]}
+      *)
       let _owned_projs, external_projs =
         List.partition (fun (abs_id', _) -> abs_id' = abs_id) projs
       in
@@ -1383,22 +1383,22 @@ and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids)
        * from this abstraction, we can end it directly, otherwise we need
        * to end the abstraction where it came from first *)
       if abs_id' = abs_id then (
-        (* Note that it happens when a function returns a `&mut ...` which gets
-         * expanded to `mut_borrow l s`, and we end the borrow `l` (so `s` gets
-         * reinjected in the parent abstraction without having been modified).
-         *
-         * The context looks like this:
-         * ```
-         * abs'0 {
-         *   [s <: ...]
-         *   (s <: ...)
-         * }
-         *
-         * // Note that `s` can't appear in other abstractions or in the
-         * // regular environment (because we forbid the duplication of
-         * // symbolic values which contain borrows).
-         * ```
-         *)
+        (* Note that it happens when a function returns a [&mut ...] which gets
+           expanded to [mut_borrow l s], and we end the borrow [l] (so [s] gets
+           reinjected in the parent abstraction without having been modified).
+
+           The context looks like this:
+           {[
+             abs'0 {
+               [s <: ...]
+               (s <: ...)
+             }
+
+             // Note that [s] can't appear in other abstractions or in the
+             // regular environment (because we forbid the duplication of
+             // symbolic values which contain borrows).
+           ]}
+        *)
         (* End the projector of borrows - TODO: not completely sure what to
          * replace it with... Maybe we should introduce an ABottomProj? *)
         let ctx = update_aproj_borrows abs_id sv V.AIgnoredProjBorrows ctx in
@@ -1439,7 +1439,7 @@ let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun =
 
     The returned value (previously shared) is checked:
     - it mustn't contain loans
-    - it mustn't contain [Bottom]
+    - it mustn't contain {!V.Bottom}
     - it mustn't contain inactivated borrows
     TODO: this kind of checks should be put in an auxiliary helper, because
     they are redundant.
@@ -1456,7 +1456,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
      ^ "\n- context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
   (* Lookup the shared loan - note that we can't promote a shared loan
    * in a shared value, but we can do it in a mutably borrowed value.
-   * This is important because we can do: `let y = &two-phase ( *x );`
+   * This is important because we can do: [let y = &two-phase ( *x );]
    *)
   let ek =
     { enter_shared_loans = false; enter_mut_borrows = true; enter_abs = false }
@@ -1471,7 +1471,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
          we should have gotten rid of those already, but it is better
          to do a sanity check. *)
       assert (not (loans_in_value sv));
-      (* Check there isn't [Bottom] (this is actually an invariant *)
+      (* Check there isn't {!Bottom} (this is actually an invariant *)
       assert (not (bottom_in_value ctx.ended_regions sv));
       (* Check there aren't inactivated borrows *)
       assert (not (inactivated_in_value sv));
@@ -1486,7 +1486,7 @@ let promote_shared_loan_to_mut_loan (l : V.BorrowId.id)
         "Can't promote a shared loan to a mutable loan if the loan is inside \
          an abstraction"
 
-(** Helper function: see [activate_inactivated_mut_borrow].
+(** Helper function: see {!activate_inactivated_mut_borrow}.
 
     This function updates a shared borrow to a mutable borrow.
  *)
@@ -1564,7 +1564,7 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
            * the borrow. *)
           let cc = comp cc (promote_shared_loan_to_mut_loan l) in
           (* Promote the borrow - the value should have been checked by
-             [promote_shared_loan_to_mut_loan]
+             {!promote_shared_loan_to_mut_loan}
           *)
           let cc =
             comp cc (fun cf borrowed_value ->
diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index f2f10944..a5501712 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -50,8 +50,8 @@ type borrow_ids_or_symbolic_value =
 
 let update_if_none opt x = match opt with None -> Some x | _ -> opt
 
-exception FoundPriority of priority_borrows_or_abs
 (** Utility exception *)
+exception FoundPriority of priority_borrows_or_abs
 
 type loan_or_borrow_content =
   | LoanContent of V.loan_content
@@ -210,6 +210,11 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
             if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
             else ()
 
+      (** We reimplement {!visit_Loan} (rather than the more precise functions
+          {!visit_SharedLoan}, etc.) on purpose: as we have an exhaustive match
+          below, we are more resilient to definition updates (the compiler
+          is our friend).
+      *)
       method! visit_loan_content env lc =
         match lc with
         | V.SharedLoan (bids, sv) ->
@@ -223,12 +228,10 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
             (* Check if this is the loan we are looking for *)
             if bid = l then raise (FoundGLoanContent (Concrete lc))
             else super#visit_MutLoan env bid
-      (** We reimplement [visit_Loan] (rather than the more precise functions
-          [visit_SharedLoan], etc.) on purpose: as we have an exhaustive match
-          below, we are more resilient to definition updates (the compiler
-          is our friend).
-      *)
 
+      (** Note that we don't control diving inside the abstractions: if we
+          allow to dive inside abstractions, we allow to go anywhere
+          (because there are no use cases requiring finer control) *)
       method! visit_aloan_content env lc =
         match lc with
         | V.AMutLoan (bid, av) ->
@@ -245,9 +248,6 @@ let lookup_loan_opt (ek : exploration_kind) (l : V.BorrowId.id)
             { given_back = _; child = _; given_back_meta = _ }
         | V.AIgnoredSharedLoan _ ->
             super#visit_aloan_content env lc
-      (** Note that we don't control diving inside the abstractions: if we
-          allow to dive inside abstractions, we allow to go anywhere
-          (because there are no use cases requiring finer control) *)
 
       method! visit_Var env bv v =
         assert (Option.is_none !abs_or_var);
@@ -318,6 +318,8 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
             if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
             else V.MutBorrow (bid, mv)
 
+      (** We reimplement {!visit_loan_content} (rather than one of the sub-
+          functions) on purpose: exhaustive matches are good for maintenance *)
       method! visit_loan_content env lc =
         match lc with
         | V.SharedLoan (bids, sv) ->
@@ -330,17 +332,15 @@ let update_loan (ek : exploration_kind) (l : V.BorrowId.id)
         | V.MutLoan bid ->
             (* Mut loan: checks if this is the loan we are looking for *)
             if bid = l then update () else super#visit_MutLoan env bid
-      (** We reimplement [visit_loan_content] (rather than one of the sub-
-          functions) on purpose: exhaustive matches are good for maintenance *)
 
-      method! visit_abs env abs =
-        if ek.enter_abs then super#visit_abs env abs else abs
       (** Note that once inside the abstractions, we don't control diving
           (there are no use cases requiring finer control).
-          Also, as we give back a [loan_content] (and not an [aloan_content])
+          Also, as we give back a {!loan_content} (and not an {!aloan_content})
           we don't need to do reimplement the visit functions for the values
           inside the abstractions (rk.: there may be "concrete" values inside
           abstractions, so there is a utility in diving inside). *)
+      method! visit_abs env abs =
+        if ek.enter_abs then super#visit_abs env abs else abs
     end
   in
 
@@ -386,10 +386,10 @@ let update_aloan (ek : exploration_kind) (l : V.BorrowId.id)
         | V.AIgnoredSharedLoan _ ->
             super#visit_aloan_content env lc
 
-      method! visit_abs env abs =
-        if ek.enter_abs then super#visit_abs env abs else abs
       (** Note that once inside the abstractions, we don't control diving
           (there are no use cases requiring finer control). *)
+      method! visit_abs env abs =
+        if ek.enter_abs then super#visit_abs env abs else abs
     end
   in
 
@@ -665,7 +665,7 @@ type looked_up_aproj_borrows =
 (** Lookup the aproj_borrows (including aproj_shared_borrows) over a
     symbolic value which intersect a given set of regions.
         
-    [lookup_shared]: if `true` also explore projectors over shared values,
+    [lookup_shared]: if [true] also explore projectors over shared values,
     otherwise ignore.
     
     This is a helper function.
@@ -754,7 +754,7 @@ let lookup_intersecting_aproj_borrows_not_shared_opt
   | Some (NonSharedProj (abs_id, rty)) -> Some (abs_id, rty)
   | _ -> failwith "Unexpected"
 
-(** Similar to [lookup_intersecting_aproj_borrows_opt], but updates the
+(** Similar to {!lookup_intersecting_aproj_borrows_opt}, but updates the
     values.
 
     This is a helper function: it might break invariants.
@@ -829,7 +829,7 @@ let update_intersecting_aproj_borrows (can_update_shared : bool)
   (* Return *)
   ctx
 
-(** Simply calls [update_intersecting_aproj_borrows] to update a
+(** Simply calls {!update_intersecting_aproj_borrows} to update a
     proj_borrows over a non-shared value.
     
     We check that we update *at least* one proj_borrows.
@@ -857,7 +857,7 @@ let update_intersecting_aproj_borrows_non_shared (regions : T.RegionId.Set.t)
   (* Return *)
   ctx
 
-(** Simply calls [update_intersecting_aproj_borrows] to remove the
+(** Simply calls {!update_intersecting_aproj_borrows} to remove the
     proj_borrows over shared values.
 
     This is a helper function: it might break invariants.
@@ -878,26 +878,26 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
     
     Note that we can update more than one projector of loans! Consider the
     following example:
-    ```
-    fn f<'a, 'b>(...) -> (&'a mut u32, &'b mut u32));
-    fn g<'c>(&'c mut u32, &'c mut u32);
-
-    let p = f(...);
-    g(move p);
-
-    // Symbolic context after the call to g:
-    // abs'a {'a} { [s@0 <: (&'a mut u32, &'b mut u32)] }
-    // abs'b {'b} { [s@0 <: (&'a mut u32, &'b mut u32)] }
-    //
-    // abs'c {'c} { (s@0 <: (&'c mut u32, &'c mut u32)) }
-    ```
+    {[
+      fn f<'a, 'b>(...) -> (&'a mut u32, &'b mut u32));
+      fn g<'c>(&'c mut u32, &'c mut u32);
+
+      let p = f(...);
+      g(move p);
+
+      // Symbolic context after the call to g:
+      // abs'a {'a} { [s@0 <: (&'a mut u32, &'b mut u32)] }
+      // abs'b {'b} { [s@0 <: (&'a mut u32, &'b mut u32)] }
+      //
+      // abs'c {'c} { (s@0 <: (&'c mut u32, &'c mut u32)) }
+    ]}
     
     Note that for sanity, this function checks that we update *at least* one
     projector of loans.
         
     [subst]: takes as parameters the abstraction in which we perform the
     substitution and the list of given back values at the projector of
-    loans where we perform the substitution (see the fields in [AProjLoans]).
+    loans where we perform the substitution (see the fields in {!V.AProjLoans}).
     Note that the symbolic value at this place is necessarily equal to [sv],
     which is why we don't give it as parameters.
  *)
@@ -942,11 +942,11 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
   (* Return *)
   ctx
 
-(** Helper function: lookup an [AProjLoans] by using an abstraction id and a
+(** Helper function: lookup an {!V.AProjLoans} by using an abstraction id and a
     symbolic value.
     
     We return the information from the looked up projector of loans. See the
-    fields in [AProjLoans] (we don't return the symbolic value, because it
+    fields in {!V.AProjLoans} (we don't return the symbolic value, because it
     is equal to [sv]).
     
     Sanity check: we check that there is exactly one projector which corresponds
@@ -1044,7 +1044,7 @@ let update_aproj_loans (abs_id : V.AbstractionId.id) (sv : V.symbolic_value)
     Sanity check: we check that there is exactly one projector which corresponds
     to the couple (abstraction id, symbolic value).
     
-    TODO: factorize with [update_aproj_loans]?
+    TODO: factorize with {!update_aproj_loans}?
  *)
 let update_aproj_borrows (abs_id : V.AbstractionId.id) (sv : V.symbolic_value)
     (nproj : V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
@@ -1087,7 +1087,7 @@ let update_aproj_borrows (abs_id : V.AbstractionId.id) (sv : V.symbolic_value)
 
 (** Helper function: might break invariants.
 
-    Converts an [AProjLoans] to an [AEndedProjLoans]. The projector is identified
+    Converts an {!V.AProjLoans} to an {!V.AEndedProjLoans}. The projector is identified
     by a symbolic value and an abstraction id.
  *)
 let update_aproj_loans_to_ended (abs_id : V.AbstractionId.id)
@@ -1150,6 +1150,7 @@ let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) :
             (* Ignore *)
             super#visit_aloan_content env lc
 
+      (** We may need to visit loan contents because of shared values *)
       method! visit_loan_content _ lc =
         match lc with
         | V.MutLoan _ ->
@@ -1157,7 +1158,6 @@ let get_first_non_ignored_aloan_in_abstraction (abs : V.abs) :
              * value in an abstraction should be in an AProjBorrows *)
             failwith "Unreachable"
         | V.SharedLoan (bids, _) -> raise (FoundBorrowIds (Borrows bids))
-      (** We may need to visit loan contents because of shared values *)
 
       method! visit_aproj env sproj =
         (match sproj with
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index c34051a8..0ca34b43 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -66,24 +66,24 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
     object (self)
       inherit [_] C.map_eval_ctx as super
 
+      (** When visiting an abstraction, we remember the regions it owns to be
+          able to properly reduce projectors when expanding symbolic values *)
       method! visit_abs current_abs abs =
         assert (Option.is_none current_abs);
         let current_abs = Some abs in
         super#visit_abs current_abs abs
-      (** When visiting an abstraction, we remember the regions it owns to be
-          able to properly reduce projectors when expanding symbolic values *)
 
+      (** We carefully updated {!visit_ASymbolic} so that {!visit_aproj} is called
+          only on child projections (i.e., projections which appear in {!AEndedProjLoans}).
+          The role of visit_aproj is then to check we don't have to expand symbolic
+          values in child projections, because it should never happen
+        *)
       method! visit_aproj current_abs aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
             assert (not (same_symbolic_id sv original_sv))
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj current_abs aproj
-      (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called
-          only on child projections (i.e., projections which appear in [AEndedProjLoans]).
-          The role of visit_aproj is then to check we don't have to expand symbolic
-          values in child projections, because it should never happen
-        *)
 
       method! visit_ASymbolic current_abs aproj =
         let current_abs = Option.get current_abs in
@@ -214,7 +214,7 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     The function might return a list of values if the symbolic value to expand
     is an enumeration.
     
-    `expand_enumerations` controls the expansion of enumerations: if false, it
+    [expand_enumerations] controls the expansion of enumerations: if false, it
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
@@ -290,8 +290,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   in
   (* Small utility used on shared borrows in abstractions (regular borrow
    * projector and asb).
-   * Returns `Some` if the symbolic value has been expanded to an asb list,
-   * `None` otherwise *)
+   * Returns [Some] if the symbolic value has been expanded to an asb list,
+   * [None] otherwise *)
   let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) :
       V.abstract_shared_borrows option =
     if same_symbolic_id sv original_sv then
@@ -341,17 +341,17 @@ let expand_symbolic_value_shared_borrow (config : C.config)
         let asb = List.concat (List.map expand_asb asb) in
         V.AProjSharedBorrow asb
 
+      (** We carefully updated {!visit_ASymbolic} so that {!visit_aproj} is called
+          only on child projections (i.e., projections which appear in {!AEndedProjLoans}).
+          The role of visit_aproj is then to check we don't have to expand symbolic
+          values in child projections, because it should never happen
+        *)
       method! visit_aproj proj_regions aproj =
         (match aproj with
         | AProjLoans (sv, _) | AProjBorrows (sv, _) ->
             assert (not (same_symbolic_id sv original_sv))
         | AEndedProjLoans _ | AEndedProjBorrows _ | AIgnoredProjBorrows -> ());
         super#visit_aproj proj_regions aproj
-      (** We carefully updated [visit_ASymbolic] so that [visit_aproj] is called
-          only on child projections (i.e., projections which appear in [AEndedProjLoans]).
-          The role of visit_aproj is then to check we don't have to expand symbolic
-          values in child projections, because it should never happen
-        *)
 
       method! visit_ASymbolic proj_regions aproj =
         match aproj with
@@ -486,7 +486,7 @@ let expand_symbolic_bool (config : C.config) (sp : V.symbolic_value)
 
 (** Expand a symbolic value.
     
-    [allow_branching]: if `true` we can branch (by expanding enumerations with
+    [allow_branching]: if [true] we can branch (by expanding enumerations with
     stricly more than one variant), otherwise we can't.
     
     TODO: rename [sp] to [sv]
@@ -588,26 +588,26 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
   (* Continue *)
   cc cf ctx
 
-(** Symbolic integers are expanded upon evaluating a `switch`, when the integer
+(** Symbolic integers are expanded upon evaluating a [switch], when the integer
     is not an enumeration discriminant.
     Note that a discriminant is never symbolic: we evaluate discriminant values
-    upon evaluating `eval_discriminant`, which always generates a concrete value
+    upon evaluating [eval_discriminant], which always generates a concrete value
     (because if we call it on a symbolic enumeration, we expand the enumeration
     *then* evaluate the discriminant). This is how we can spot "regular" switches
     over integers.
 
 
-    When expanding a boolean upon evaluating an `if ... then ... else ...`,
+    When expanding a boolean upon evaluating an [if ... then ... else ...],
     or an enumeration just before matching over it, we can simply expand the
     boolean/enumeration (generating a list of contexts from which to execute)
-    then retry evaluating the `if ... then ... else ...` or the `match`: as
+    then retry evaluating the [if ... then ... else ...] or the [match]: as
     the scrutinee will then have a concrete value, the interpreter will switch
     to the proper branch.
     
     However, when expanding a "regular" integer for a switch, there is always an
     *otherwise* branch that we can take, for which the integer must remain symbolic
     (because in this branch the scrutinee can take a range of values). We thus
-    can't simply expand then retry to evaluate the `switch`, because then we
+    can't simply expand then retry to evaluate the [switch], because then we
     would loop...
     
     For this reason, we take the list of branches to execute as parameters, and
@@ -661,8 +661,8 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
           raise (FoundSymbolicValue sv)
         else ()
 
-      method! visit_abs _ _ = ()
       (** Don't enter abstractions *)
+      method! visit_abs _ _ = ()
     end
   in
 
@@ -681,7 +681,7 @@ let greedy_expand_symbolics_with_borrows (config : C.config) : cm_fun =
       let cc : cm_fun =
         match sv.V.sv_ty with
         | T.Adt (AdtId def_id, _, _) ->
-            (* [expand_symbolic_value_no_branching] checks if there are branchings,
+            (* {!expand_symbolic_value_no_branching} checks if there are branchings,
              * but we prefer to also check it here - this leads to cleaner messages
              * and debugging *)
             let def = C.ctx_lookup_type_decl ctx def_id in
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index 4a4f3353..62d9b80b 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -73,7 +73,7 @@ let read_place (config : C.config) (access : access_kind) (p : E.place)
 
     We reorganize the environment so that:
     - we can access the place (we prepare *along* the path)
-    - the value at the place itself doesn't contain loans (the `access_kind`
+    - the value at the place itself doesn't contain loans (the [access_kind]
       controls whether we only end mutable loans, or also shared loans).
 
     We also check, after the reorganization, that the value at the place
@@ -138,17 +138,17 @@ let constant_to_typed_value (ty : T.ety) (cv : V.constant_value) : V.typed_value
     
     Sometimes, we want to decouple the two operations.
     Consider the following example:
-    ```
-    context = {
-      x -> shared_borrow l0
-      y -> shared_loan {l0} v
-    }
-    
-    dest <- f(move x, move y);
-    ...
-    ```
-    Because of the way `end_borrow` is implemented, when giving back the borrow
-    `l0` upon evaluating `move y`, we won't notice that `shared_borrow l0` has
+    {[
+      context = {
+        x -> shared_borrow l0
+        y -> shared_loan {l0} v
+      }
+
+      dest <- f(move x, move y);
+      ...
+    ]}
+    Because of the way [end_borrow] is implemented, when giving back the borrow
+    [l0] upon evaluating [move y], we won't notice that [shared_borrow l0] has
     disappeared from the environment (it has been moved and not assigned yet,
     and so is hanging in "thin air").
     
@@ -247,7 +247,7 @@ let eval_operand_no_reorganize (config : C.config) (op : E.operand)
     **Warning**: this function shouldn't be used to evaluate a list of
     operands (for a function call, for instance): we must do *one* reorganization
     of the environment, before evaluating all the operands at once.
-    Use [`eval_operands`] instead.
+    Use [eval_operands] instead.
  *)
 let eval_operand (config : C.config) (op : E.operand)
     (cf : V.typed_value -> m_fun) : m_fun =
@@ -497,7 +497,7 @@ let eval_binary_op (config : C.config) (binop : E.binop) (op1 : E.operand)
 (** Evaluate the discriminant of a concrete (i.e., non symbolic) ADT value *)
 let eval_rvalue_discriminant_concrete (config : C.config) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
-  (* Note that discriminant values have type `isize` *)
+  (* Note that discriminant values have type [isize] *)
   (* Access the value *)
   let access = Read in
   let expand_prim_copy = false in
@@ -537,7 +537,7 @@ let eval_rvalue_discriminant (config : C.config) (p : E.place)
     (cf : V.typed_value -> m_fun) : m_fun =
  fun ctx ->
   log#ldebug (lazy "eval_rvalue_discriminant");
-  (* Note that discriminant values have type `isize` *)
+  (* Note that discriminant values have type [isize] *)
   (* Access the value *)
   let access = Read in
   let expand_prim_copy = false in
diff --git a/src/InterpreterPaths.ml b/src/InterpreterPaths.ml
index 16ab9aad..d54a046e 100644
--- a/src/InterpreterPaths.ml
+++ b/src/InterpreterPaths.ml
@@ -174,7 +174,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                     | Error err -> Error err
                     | Ok (ctx, res) ->
                         (* Update the shared loan with the new value returned
-                           by [access_projection] *)
+                           by {!access_projection} *)
                         let ctx =
                           update_loan ek bid
                             (V.SharedLoan (bids, res.updated))
@@ -205,7 +205,7 @@ let rec access_projection (access : projection_access) (ctx : C.eval_ctx)
                           | _ -> failwith "Unexpected"
                         in
                         (* Update the shared loan with the new value returned
-                             by [access_projection] *)
+                             by {!access_projection} *)
                         let ctx =
                           update_aloan ek bid
                             (V.ASharedLoan (bids, res.updated, av))
@@ -378,7 +378,7 @@ let compute_expanded_bottom_adt_value (tyctx : T.type_decl T.TypeDeclId.Map.t)
 (** Compute an expanded Option bottom value *)
 let compute_expanded_bottom_option_value (variant_id : T.VariantId.id)
     (param_ty : T.ety) : V.typed_value =
-  (* Note that the variant can be `Some` or `None`: we expand bottom values
+  (* Note that the variant can be [Some] or [None]: we expand bottom values
    * when writing to fields or setting discriminants *)
   let field_values =
     if variant_id = T.option_some_id then [ mk_bottom param_ty ]
@@ -398,23 +398,23 @@ let compute_expanded_bottom_tuple_value (field_types : T.ety list) :
   let ty = T.Adt (T.Tuple, [], field_types) in
   { V.value = v; V.ty }
 
-(** Auxiliary helper to expand [Bottom] values.
+(** Auxiliary helper to expand {!V.Bottom} values.
 
     During compilation, rustc desaggregates the ADT initializations. The
     consequence is that the following rust code:
-    ```
-    let x = Cons a b;
-    ```
+    {[
+      let x = Cons a b;
+    ]}
 
     Looks like this in MIR:
-    ```
-    (x as Cons).0 = a;
-    (x as Cons).1 = b;
-    set_discriminant(x, 0); // If `Cons` is the variant of index 0
-    ```
+    {[
+      (x as Cons).0 = a;
+      (x as Cons).1 = b;
+      set_discriminant(x, 0); // If [Cons] is the variant of index 0
+    ]}
 
     The consequence is that we may sometimes need to write fields to values
-    which are currently [Bottom]. When doing this, we first expand the value
+    which are currently {!V.Bottom}. When doing this, we first expand the value
     to, say, [Cons Bottom Bottom] (note that field projection contains information
     about which variant we should project to, which is why we *can* set the
     variant index when writing one of its fields).
@@ -436,12 +436,12 @@ let expand_bottom_value_from_projection (config : C.config)
   in
   let p' = { p with projection = projection' } in
   (* Compute the expanded value.
-     The type of the [Bottom] value should be a tuple or an ADT.
+     The type of the {!V.Bottom} value should be a tuple or an ADT.
      Note that the projection element we got stuck at should be a
-     field projection, and gives the variant id if the [Bottom] value
+     field projection, and gives the variant id if the {!V.Bottom} value
      is an enumeration value.
      Also, the expanded value should be the proper ADT variant or a tuple
-     with the proper arity, with all the fields initialized to [Bottom]
+     with the proper arity, with all the fields initialized to {!V.Bottom}
   *)
   let nv =
     match (pe, ty) with
@@ -500,7 +500,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
             expand_symbolic_value_no_branching config sp
               (Some (Synth.mk_mplace prefix ctx))
         | FailBottom (_, _, _) ->
-            (* We can't expand [Bottom] values while reading them *)
+            (* We can't expand {!V.Bottom} values while reading them *)
             failwith "Found [Bottom] while reading a place"
         | FailBorrow _ -> failwith "Could not read a borrow"
       in
@@ -508,7 +508,7 @@ let rec update_ctx_along_read_place (config : C.config) (access : access_kind)
 
 (** Update the environment to be able to write to a place.
 
-    See [update_env_alond_read_place].
+    See {!update_ctx_along_read_place}.
 *)
 let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
     (p : E.place) : cm_fun =
@@ -530,7 +530,7 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
             expand_symbolic_value_no_branching config sp
               (Some (Synth.mk_mplace p ctx))
         | FailBottom (remaining_pes, pe, ty) ->
-            (* Expand the [Bottom] value *)
+            (* Expand the {!V.Bottom} value *)
             fun cf ctx ->
              let ctx =
                expand_bottom_value_from_projection config access p remaining_pes
@@ -542,14 +542,14 @@ let rec update_ctx_along_write_place (config : C.config) (access : access_kind)
       (* Retry *)
       comp cc (update_ctx_along_write_place config access p) cf ctx
 
-exception UpdateCtx of cm_fun
 (** Small utility used to break control-flow *)
+exception UpdateCtx of cm_fun
 
 (** End the loans at a given place: read the value, if it contains a loan,
     end this loan, repeat.
 
     This is used when reading or borrowing values. We typically
-    first call [update_ctx_along_read_place] or [update_ctx_along_write_place]
+    first call {!update_ctx_along_read_place} or {!update_ctx_along_write_place}
     to get access to the value, then call this function to "prepare" the value:
     when moving values, we can't move a value which contains loans and thus need
     to end them, etc.
@@ -620,7 +620,7 @@ let rec end_loans_at_place (config : C.config) (access : access_kind)
     
     [end_borrows]:
     - if true: end all the loans and borrows we find, starting with the outer
-      ones. This is used when evaluating the `drop` statement (see [drop_value])
+      ones. This is used when evaluating the [drop] statement (see [drop_value])
     - if false: only end the outer loans. This is used by [assign_to_place]
       or to drop the loans in the local variables when popping a frame.
 
@@ -766,7 +766,7 @@ let rec copy_value (allow_adt_copy : bool) (config : C.config)
 
     Return the updated context and the (updated) value at the end of the
     place. This value should not contain any loan or borrow (and we check
-    it is the case). Note that this value is very likely to contain [Bottom]
+    it is the case). Note that this value is very likely to contain {!V.Bottom}
     subvalues.
     
     [end_borrows]: if false, we only end the outer loans we find. If true, we
diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml
index 76b7d6ae..064b8969 100644
--- a/src/InterpreterProjectors.ml
+++ b/src/InterpreterProjectors.ml
@@ -12,7 +12,7 @@ open InterpreterBorrowsCore
 
     Apply a proj_borrows on a shared borrow.
     Note that when projecting over shared values, we generate
-    [abstract_shared_borrows], not avalues.
+    {!V.abstract_shared_borrows}, not {!V.avalue}s.
 *)
 let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
     (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
@@ -22,7 +22,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
    * recursive call which is a bit overkill...) *)
   let ety = Subst.erase_regions ty in
   assert (ety = v.V.ty);
-  (* Project - if there are no regions from the abstraction in the type, return `_` *)
+  (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then []
   else
     match (v.V.value, ty) with
@@ -97,12 +97,12 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
     - [v]: the value over which we project
     - [ty]: the projection type (is used to map borrows to regions, or to
       interpret the borrows as belonging to some regions...). Remember that
-      `v` doesn't contain region information.
+      [v] doesn't contain region information.
       For instance, if we have:
-      `v <: ty` where:
-      - `v = mut_borrow l ...`
-      - `ty = Ref (r, ...)`
-      then we interpret the borrow `l` as belonging to region `r`
+      [v <: ty] where:
+      - [v = mut_borrow l ...]
+      - [ty = Ref (r, ...)]
+      then we interpret the borrow [l] as belonging to region [r]
     
     Also, when applying projections on shared values, we need to apply
     reborrows. This is a bit annoying because, with the way we compute
@@ -115,13 +115,13 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx)
     This check is activated when applying projectors upon calling a function
     (because we need to check that function arguments don't contain ⊥),
     but deactivated when expanding symbolic values:
-    ```
-    fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
-    
-    let p = f(&mut x, &mut y); // p -> @s0
-    assert(x == ...); // end 'a
-    let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
-    ```
+    {[
+      fn f<'a,'b>(x : &'a mut u32, y : &'b mut u32) -> (&'a mut u32, &'b mut u32);
+
+      let p = f(&mut x, &mut y); // p -> @s0
+      assert(x == ...); // end 'a
+      let z = p.1; // HERE: the symbolic expansion of @s0 contains ended regions
+    ]}
 *)
 let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
     (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id)
@@ -131,7 +131,7 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx)
    * recursive call which is a bit overkill...) *)
   let ety = Substitute.erase_regions ty in
   assert (ety = v.V.ty);
-  (* Project - if there are no regions from the abstraction in the type, return `_` *)
+  (* Project - if there are no regions from the abstraction in the type, return [_] *)
   if not (ty_has_regions_in_set regions ty) then { V.value = V.AIgnored; ty }
   else
     let value : V.avalue =
@@ -343,18 +343,18 @@ let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t)
     This function is used when applying projectors on shared borrows: when
     doing so, we might need to reborrow subvalues from the shared value.
     For instance:
-    ```
-    fn f<'a,'b,'c>(x : &'a 'b 'c u32)
-    ```
+    {[
+      fn f<'a,'b,'c>(x : &'a 'b 'c u32)
+    ]}
     When introducing the abstractions for 'a, 'b and 'c, we apply a projector
-    on some value `shared_borrow l : &'a &'b &'c u32`.
+    on some value [shared_borrow l : &'a &'b &'c u32].
     In the 'a abstraction, this shared borrow gets projected. However, when
     reducing the projectors for the 'b and 'c abstractions, we need to make
     sure that the borrows living in regions 'b and 'c live as long as those
     regions. This is done by looking up the shared value and applying reborrows
     on the borrows we find there (note that those reborrows apply on shared
     borrows - easy - and mutable borrows - in this case, we reborrow the whole
-    borrow: `mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)`).
+    borrow: [mut_borrow ... ~~> shared_loan {...} (mut_borrow ...)]).
 *)
 let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
     (ctx : C.eval_ctx) : C.eval_ctx =
@@ -415,6 +415,8 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
     object
       inherit [_] C.map_eval_ctx as super
 
+      (** We may need to reborrow mutable borrows. Note that this doesn't
+          happen for aborrows *)
       method! visit_typed_value env v =
         match v.V.value with
         | V.Borrow (V.MutBorrow (bid, bv)) ->
@@ -430,9 +432,9 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
               let ty = v.V.ty in
               { V.value; ty }
         | _ -> super#visit_typed_value env v
-      (** We may need to reborrow mutable borrows. Note that this doesn't
-          happen for aborrows *)
 
+      (** We reimplement {!visit_loan_content} (rather than one of the sub-
+          functions) on purpose: exhaustive matches are good for maintenance *)
       method! visit_loan_content env lc =
         match lc with
         | V.SharedLoan (bids, sv) ->
@@ -455,8 +457,6 @@ let apply_reborrows (reborrows : (V.BorrowId.id * V.BorrowId.id) list)
         | V.MutLoan bid ->
             (* Nothing special to do *)
             super#visit_MutLoan env bid
-      (** We reimplement [visit_loan_content] (rather than one of the sub-
-          functions) on purpose: exhaustive matches are good for maintenance *)
 
       method! visit_aloan_content env lc =
         match lc with
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 275a6c58..4e61e683 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -28,12 +28,12 @@ let drop_value (config : C.config) (p : E.place) : cm_fun =
       ("drop_value: place: " ^ place_to_string ctx p ^ "\n- Initial context:\n"
      ^ eval_ctx_to_string ctx));
   (* Prepare the place (by ending the outer loans).
-   * Note that [prepare_lplace] will use the `Write` access kind:
-   * it is ok, because when updating the value with [Bottom] below,
-   * we will use the `Move` access *)
+   * Note that {!prepare_lplace} will use the [Write] access kind:
+   * it is ok, because when updating the value with {!Bottom} below,
+   * we will use the [Move] access *)
   let end_borrows = false in
   let prepare = prepare_lplace config end_borrows p in
-  (* Replace the value with [Bottom] *)
+  (* Replace the value with {!Bottom} *)
   let replace cf (v : V.typed_value) ctx =
     (* Move the value at destination (that we will overwrite) to a dummy variable
      * to preserve the borrows *)
@@ -157,8 +157,8 @@ let eval_assertion_concrete (config : C.config) (assertion : A.assertion) :
 (** Evaluates an assertion.
     
     In the case the boolean under scrutinee is symbolic, we synthesize
-    a call to `assert ...` then continue in the success branch (and thus
-    expand the boolean to `true`).
+    a call to [assert ...] then continue in the success branch (and thus
+    expand the boolean to [true]).
  *)
 let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
  fun cf ctx ->
@@ -203,10 +203,10 @@ let eval_assertion (config : C.config) (assertion : A.assertion) : st_cm_fun =
     - either the discriminant is already the proper one (in which case we
       don't do anything)
     - or it is not the proper one (because the variant is not the proper
-      one, or the value is actually [Bottom] - this happens when
+      one, or the value is actually {!V.Bottom} - this happens when
       initializing ADT values), in which case we replace the value with
-      a variant with all its fields set to [Bottom].
-      For instance, something like: `Cons Bottom Bottom`.
+      a variant with all its fields set to {!V.Bottom}.
+      For instance, something like: [Cons Bottom Bottom].
  *)
 let set_discriminant (config : C.config) (p : E.place)
     (variant_id : T.VariantId.id) : st_cm_fun =
@@ -232,7 +232,7 @@ let set_discriminant (config : C.config) (p : E.place)
            - either the discriminant is already the proper one (in which case we
              don't do anything)
            - or it is not the proper one, in which case we replace the value with
-             a variant with all its fields set to [Bottom]
+             a variant with all its fields set to {!Bottom}
         *)
         match av.variant_id with
         | None -> raise (Failure "Found a struct value while expected an enum")
@@ -297,7 +297,7 @@ let push_frame : cm_fun = fun cf ctx -> cf (ctx_push_frame ctx)
  *)
 let get_non_local_function_return_type (fid : A.assumed_fun_id)
     (region_params : T.erased_region list) (type_params : T.ety list) : T.ety =
-  (* `Box::free` has a special treatment *)
+  (* [Box::free] has a special treatment *)
   match (fid, region_params, type_params) with
   | A.BoxFree, [], [ _ ] -> mk_unit_ty
   | _ ->
@@ -322,7 +322,7 @@ let move_return_value (config : C.config) (cf : V.typed_value -> m_fun) : m_fun
     
     Drop all the local variables but the return variable, move the return
     value out of the return variable, remove all the local variables (but not the
-    abstractions!) from the context, remove the [Frame] indicator delimiting the
+    abstractions!) from the context, remove the {!C.Frame} indicator delimiting the
     current frame and handle the return value to the continuation.
     
     TODO: rename (remove the "ctx_")
@@ -385,7 +385,7 @@ let ctx_pop_frame (config : C.config) (cf : V.typed_value -> m_fun) : m_fun =
            ^ eval_ctx_to_string ctx)))
   in
 
-  (* Pop the frame - we remove the `Frame` delimiter, and reintroduce all
+  (* Pop the frame - we remove the [Frame] delimiter, and reintroduce all
    * the local variables (which may still contain borrow permissions - but
    * no outer loans) as dummy variables in the caller frame *)
   let rec pop env =
@@ -457,8 +457,8 @@ let eval_box_new_concrete (config : C.config)
       comp cf_move cf_create cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function which factorizes code to evaluate `std::Deref::deref`
-    and `std::DerefMut::deref_mut` - see [eval_non_local_function_call] *)
+(** Auxiliary function which factorizes code to evaluate [std::Deref::deref]
+    and [std::DerefMut::deref_mut] - see [eval_non_local_function_call] *)
 let eval_box_deref_mut_or_shared_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list)
     (is_mut : bool) : cm_fun =
@@ -517,22 +517,22 @@ let eval_box_deref_mut_concrete (config : C.config)
 
 (** Auxiliary function - see [eval_non_local_function_call].
 
-    `Box::free` is not handled the same way as the other assumed functions:
+    [Box::free] is not handled the same way as the other assumed functions:
     - in the regular case, whenever we need to evaluate an assumed function,
       we evaluate the operands, push a frame, call a dedicated function
       to correctly update the variables in the frame (and mimic the execution
       of a body) and finally pop the frame
-    - in the case of `Box::free`: the value given to this function is often
-      of the form `Box(⊥)` because we can move the value out of the
+    - in the case of [Box::free]: the value given to this function is often
+      of the form [Box(⊥)] because we can move the value out of the
       box before freeing the box. It makes it invalid to see box_free as a
       "regular" function: it is not valid to call a function with arguments
-      which contain `⊥`. For this reason, we execute `Box::free` as drop_value,
+      which contain [⊥]. For this reason, we execute [Box::free] as drop_value,
       but this is a bit annoying with regards to the semantics...
 
     Followingly this function doesn't behave like the others: it does not expect
-    a stack frame to have been pushed, but rather simply behaves like [drop_value].
-    It thus updates the box value (by calling [drop_value]) and updates
-    the destination (by setting it to `()`).
+    a stack frame to have been pushed, but rather simply behaves like {!drop_value}.
+    It thus updates the box value (by calling {!drop_value}) and updates
+    the destination (by setting it to [()]).
 *)
 let eval_box_free (config : C.config) (region_params : T.erased_region list)
     (type_params : T.ety list) (args : E.operand list) (dest : E.place) : cm_fun
@@ -548,7 +548,7 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
       (* Drop the value *)
       let cc = drop_value config input_box_place in
 
-      (* Update the destination by setting it to `()` *)
+      (* Update the destination by setting it to [()] *)
       let cc = comp cc (assign_to_place config mk_unit_value dest) in
 
       (* Continue *)
@@ -569,7 +569,7 @@ let eval_non_local_function_call_concrete (config : C.config)
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
      - the function is box_free
-     See [eval_box_free]
+     See {!eval_box_free}
   *)
   match fid with
   | A.BoxFree ->
@@ -583,8 +583,8 @@ let eval_non_local_function_call_concrete (config : C.config)
 
       (* Evaluate the call
        *
-       * Style note: at some point we used [comp_transmit] to
-       * transmit the result of [eval_operands] above down to [push_vars]
+       * Style note: at some point we used {!comp_transmit} to
+       * transmit the result of {!eval_operands} above down to {!push_vars}
        * below, without having to introduce an intermediary function call,
        * but it made it less clear where the computed values came from,
        * so we reversed the modifications. *)
@@ -668,7 +668,7 @@ let instantiate_fun_sig (type_params : T.ety list) (sg : A.fun_sig) :
   let _, rsubst, _ = Subst.fresh_regions_with_substs sg.region_params in
   (* Generate the type substitution
    * Note that we need the substitution to map the type variables to
-   * [rty] types (not [ety]). In order to do that, we convert the
+   * {!rty} types (not {!ety}). In order to do that, we convert the
    * type parameters to types with regions. This is possible only
    * if those types don't contain any regions.
    * This is a current limitation of the analysis: there is still some
@@ -697,7 +697,7 @@ let create_empty_abstractions_from_abs_region_groups (call_id : V.FunCallId.id)
     (kind : V.abs_kind) (rgl : A.abs_region_group list)
     (region_can_end : T.RegionGroupId.id -> bool) : V.abs list =
   (* We use a reference to progressively create a map from abstraction ids
-   * to set of ancestor regions. Note that abs_to_ancestors_regions[abs_id]
+   * to set of ancestor regions. Note that {!abs_to_ancestors_regions} [abs_id]
    * returns the union of:
    * - the regions of the ancestors of abs_id
    * - the regions of abs_id
@@ -887,7 +887,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
            - exits the loop
            - other...
 
-           We need a specific function because of the [Continue] case: in case we
+           We need a specific function because of the {!Continue} case: in case we
            continue, we might have to reevaluate the current loop body with the
            new context (and repeat this an indefinite number of times).
         *)
@@ -908,8 +908,8 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
               (* We can't get there.
                * Note that if we decide not to fail here but rather do
                * the same thing as for [Continue 0], we could make the
-               * code slightly simpler: calling [reeval_loop_body] with
-               * [Unit] would account for the first iteration of the loop.
+               * code slightly simpler: calling {!reeval_loop_body} with
+               * {!Unit} would account for the first iteration of the loop.
                * We prefer to write it this way for consistency and sanity,
                * though. *)
               raise (Failure "Unreachable")
@@ -933,7 +933,7 @@ and eval_global (config : C.config) (dest : V.VarId.id)
         cf ctx
   | SymbolicMode ->
       (* Generate a fresh symbolic value. In the translation, this fresh symbolic value will be
-       * defined as equal to the value of the global (see `S.synthesize_global_eval`). *)
+       * defined as equal to the value of the global (see {!S.synthesize_global_eval}). *)
       let sval =
         mk_fresh_symbolic_value V.Global (ety_no_regions_to_rty global.ty)
       in
@@ -1068,7 +1068,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
   assert (List.length args = body.A.arg_count);
   let cc = eval_operands config args in
 
-  (* Push a frame delimiter - we use [comp_transmit] to transmit the result
+  (* Push a frame delimiter - we use {!comp_transmit} to transmit the result
    * of the operands evaluation from above to the functions afterwards, while
    * ignoring it in this function *)
   let cc = comp_transmit cc push_frame in
@@ -1095,7 +1095,7 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
   in
   let cc = comp cc cf_push_inputs in
 
-  (* 3. Push the remaining local variables (initialized as [Bottom]) *)
+  (* 3. Push the remaining local variables (initialized as {!Bottom}) *)
   let cc = comp cc (push_uninitialized_vars locals) in
 
   (* Execute the function body *)
@@ -1255,7 +1255,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   (* Try to end the abstractions with no loans if:
    * - the option is enabled
    * - the function returns unit
-   * (see the documentation of [config] for more information)
+   * (see the documentation of {!config} for more information)
    *)
   let cc =
     if config.return_unit_end_abs_with_no_loans && ty_is_unit inst_sg.output
@@ -1264,7 +1264,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
   in
 
   (* Continue - note that we do as if the function call has been successful,
-   * by giving [Unit] to the continuation, because we place us in the case
+   * by giving {!Unit} to the continuation, because we place us in the case
    * where we haven't panicked. Of course, the translation needs to take the
    * panic case into account... *)
   cc (cf Unit) ctx
@@ -1285,7 +1285,7 @@ and eval_non_local_function_call_symbolic (config : C.config)
   (* There are two cases (and this is extremely annoying):
      - the function is not box_free
      - the function is box_free
-       See [eval_box_free]
+       See {!eval_box_free}
   *)
   match fid with
   | A.BoxFree ->
@@ -1309,7 +1309,7 @@ and eval_non_local_function_call_symbolic (config : C.config)
       eval_function_call_symbolic_from_inst_sig config (A.Assumed fid) inst_sig
         region_args type_args args dest cf ctx
 
-(** Evaluate a non-local (i.e, assumed) function call such as `Box::deref`
+(** Evaluate a non-local (i.e, assumed) function call such as [Box::deref]
     (auxiliary helper for [eval_statement]) *)
 and eval_non_local_function_call (config : C.config) (fid : A.assumed_fun_id)
     (region_args : T.erased_region list) (type_args : T.ety list)
@@ -1356,7 +1356,7 @@ and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
  fun cf ctx ->
   let cc = eval_statement config body in
   let cf_finish cf res =
-    (* Note that we *don't* check the result ([Panic], [Return], etc.): we
+    (* Note that we *don't* check the result ({!Panic}, {!Return}, etc.): we
      * delegate the check to the caller. *)
     (* Expand the symbolic values if necessary - we need to do that before
      * checking the invariants *)
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index fed5ff9b..e6033e9e 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -66,7 +66,7 @@ let mk_typed_value_from_symbolic_value (svalue : V.symbolic_value) :
 (** Create a loans projector value from a symbolic value.
     
     Checks if the projector will actually project some regions. If not,
-    returns [AIgnored] (`_`).
+    returns {!V.AIgnored} ([_]).
     
     TODO: update to handle 'static
  *)
@@ -118,31 +118,31 @@ let remove_borrow_from_asb (bid : V.BorrowId.id)
     contents when we perform environment lookups by using borrow ids) *)
 type ('a, 'b) concrete_or_abs = Concrete of 'a | Abstract of 'b
 
-type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
 (** Generic loan content: concrete or abstract *)
+type g_loan_content = (V.loan_content, V.aloan_content) concrete_or_abs
 
-type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
 (** Generic borrow content: concrete or abstract *)
+type g_borrow_content = (V.borrow_content, V.aborrow_content) concrete_or_abs
 
 type abs_or_var_id = AbsId of V.AbstractionId.id | VarId of V.VarId.id option
 
-exception FoundBorrowContent of V.borrow_content
 (** Utility exception *)
+exception FoundBorrowContent of V.borrow_content
 
-exception FoundLoanContent of V.loan_content
 (** Utility exception *)
+exception FoundLoanContent of V.loan_content
 
-exception FoundABorrowContent of V.aborrow_content
 (** Utility exception *)
+exception FoundABorrowContent of V.aborrow_content
 
-exception FoundGBorrowContent of g_borrow_content
 (** Utility exception *)
+exception FoundGBorrowContent of g_borrow_content
 
-exception FoundGLoanContent of g_loan_content
 (** Utility exception *)
+exception FoundGLoanContent of g_loan_content
 
-exception FoundAProjBorrows of V.symbolic_value * T.rty
 (** Utility exception *)
+exception FoundAProjBorrows of V.symbolic_value * T.rty
 
 let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) :
     bool =
@@ -187,7 +187,7 @@ let symbolic_value_has_ended_regions (ended_regions : T.RegionId.Set.t)
   let regions = rty_regions s.V.sv_ty in
   not (T.RegionId.Set.disjoint regions ended_regions)
 
-(** Check if a [value] contains ⊥.
+(** Check if a {!type:V.value} contains [⊥].
 
     Note that this function is very general: it also checks wether
     symbolic values contain already ended regions.
diff --git a/src/Invariants.ml b/src/Invariants.ml
index ef255010..4a3364a6 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -385,7 +385,7 @@ let check_constant_value_type (cv : V.constant_value) (ty : T.ety) : unit =
 
 let check_typing_invariant (ctx : C.eval_ctx) : unit =
   (* TODO: the type of aloans doens't make sense: they have a type
-   * of the shape `& (mut) T` where they should have type `T`...
+   * of the shape [& (mut) T] where they should have type [T]...
    * This messes a bit the type invariant checks when checking the
    * children. In order to isolate the problem (for future modifications)
    * we introduce function, so that we can easily spot all the involved
@@ -491,7 +491,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
         (* Continue exploring to inspect the subterms *)
         super#visit_typed_value info tv
 
-      (* TODO: there is a lot of duplication with [visit_typed_value]
+      (* TODO: there is a lot of duplication with {!visit_typed_value}
        * which is quite annoying. There might be a way of factorizing
        * that by factorizing the definitions of value and avalue, but
        * the generation of visitors then doesn't work properly (TODO:
@@ -607,14 +607,14 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit =
                 let ty2 = Subst.erase_regions sv.V.sv_ty in
                 assert (ty1 = ty2);
                 (* Also check that the symbolic values contain regions of interest -
-                 * otherwise they should have been reduced to `_` *)
+                 * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
                 assert (ty_has_regions_in_set abs.regions sv.V.sv_ty)
             | V.AProjBorrows (sv, proj_ty) ->
                 let ty2 = Subst.erase_regions sv.V.sv_ty in
                 assert (ty1 = ty2);
                 (* Also check that the symbolic values contain regions of interest -
-                 * otherwise they should have been reduced to `_` *)
+                 * otherwise they should have been reduced to [_] *)
                 let abs = Option.get info in
                 assert (ty_has_regions_in_set abs.regions proj_ty)
             | V.AEndedProjLoans (_msv, given_back_ls) ->
@@ -787,7 +787,7 @@ let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit =
     check_symbolic_values config ctx)
   else log#ldebug (lazy "Not checking invariants (check is not activated)")
 
-(** Same as [check_invariants], but written in CPS *)
+(** Same as {!check_invariants}, but written in CPS *)
 let cf_check_invariants (config : C.config) : cm_fun =
  fun cf ctx ->
   check_invariants config ctx;
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index cecd3594..1b08f1ea 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -19,19 +19,19 @@ type var = {
 [@@deriving show]
 
 type assumed_fun_id =
-  | Replace  (** `core::mem::replace` *)
+  | Replace  (** [core::mem::replace] *)
   | BoxNew
-  | BoxDeref  (** `core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref` *)
+  | BoxDeref  (** [core::ops::deref::Deref::<alloc::boxed::Box<T>>::deref] *)
   | BoxDerefMut
-      (** `core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut` *)
+      (** [core::ops::deref::DerefMut::<alloc::boxed::Box<T>>::deref_mut] *)
   | BoxFree
   | VecNew
   | VecPush
   | VecInsert
   | VecLen
-  | VecIndex  (** `core::ops::index::Index::index<alloc::vec::Vec<T>, usize>` *)
+  | VecIndex  (** [core::ops::index::Index::index<alloc::vec::Vec<T>, usize>] *)
   | VecIndexMut
-      (** `core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>` *)
+      (** [core::ops::index::IndexMut::index_mut<alloc::vec::Vec<T>, usize>] *)
 [@@deriving show, ord]
 
 type fun_id = Regular of FunDeclId.id | Assumed of assumed_fun_id
@@ -142,7 +142,7 @@ and raw_statement =
           *)
   | Continue of int
       (** Continue to (outer) loop. The loop identifier works
-          the same way as for [Break] *)
+          the same way as for {!Break} *)
   | Nop
   | Sequence of statement * statement
   | Switch of operand * switch_targets
@@ -152,9 +152,9 @@ and switch_targets =
   | If of statement * statement  (** Gives the "if" and "else" blocks *)
   | SwitchInt of integer_type * (scalar_value list * statement) list * statement
       (** The targets for a switch over an integer are:
-          - the list `(matched values, statement to execute)`
+          - the list [(matched values, statement to execute)]
             We need a list for the matched values in case we do something like this:
-            `switch n { 0 | 1 => ..., _ => ... }
+            [switch n { 0 | 1 => ..., _ => ... }]
           - the "otherwise" statement
           Also note that we precise the type of the integer (uint32, int64, etc.)
           which we switch on. *)
@@ -165,7 +165,7 @@ and switch_targets =
         name = "iter_statement";
         variety = "iter";
         ancestors = [ "iter_statement_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -173,7 +173,7 @@ and switch_targets =
         name = "map_statement";
         variety = "map";
         ancestors = [ "map_statement_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
 
diff --git a/src/LlbcAstUtils.ml b/src/LlbcAstUtils.ml
index 0e679fca..46711d0a 100644
--- a/src/LlbcAstUtils.ml
+++ b/src/LlbcAstUtils.ml
@@ -2,7 +2,7 @@ open LlbcAst
 open Utils
 module T = Types
 
-(** Check if a [statement] contains loops *)
+(** Check if a {!type:LlbcAst.statement} contains loops *)
 let statement_has_loops (st : statement) : bool =
   let obj =
     object
@@ -15,7 +15,7 @@ let statement_has_loops (st : statement) : bool =
     false
   with Found -> true
 
-(** Check if a [fun_decl] contains loops *)
+(** Check if a {!type:LlbcAst.fun_decl} contains loops *)
 let fun_decl_has_loops (fd : fun_decl) : bool =
   match fd.body with
   | Some body -> statement_has_loops body.body
@@ -56,7 +56,7 @@ let rec list_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id) :
   in
   parents
 
-(** Small utility: same as [list_parent_region_groups], but returns an ordered list.  *)
+(** Small utility: same as {!list_parent_region_groups}, but returns an ordered list.  *)
 let list_ordered_parent_region_groups (sg : fun_sig) (gid : T.RegionGroupId.id)
     : T.RegionGroupId.id list =
   let pset = list_parent_region_groups sg gid in
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 8598962e..79c9b756 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -1,8 +1,8 @@
 (** Functions to load LLBC ASTs from json.
 
-    Initially, we used `ppx_derive_yojson` to automate this.
-    However, `ppx_derive_yojson` expects formatting to be slightly
-    different from what `serde_rs` generates (because it uses [Yojson.Safe.t]
+    Initially, we used [ppx_derive_yojson] to automate this.
+    However, [ppx_derive_yojson] expects formatting to be slightly
+    different from what [serde_rs] generates (because it uses [Yojson.Safe.t]
     and not [Yojson.Basic.t]).
 
     TODO: we should check all that the integer values are in the proper range
@@ -349,7 +349,7 @@ let big_int_of_json (js : json) : (V.big_int, string) result =
     | `String is -> Ok (Z.of_string is)
     | _ -> Error "")
 
-(** Deserialize a [scalar_value] from JSON and **check the ranges**.
+(** Deserialize a {!V.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
@@ -764,12 +764,12 @@ let fun_decl_of_json (id_to_file : id_to_file_map) (js : json) :
           { A.def_id; meta; name; signature; body; is_global_decl_body = false }
     | _ -> Error "")
 
-(* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
+(* Strict type for the number of function declarations (see {!global_to_fun_id} below) *)
 type global_id_converter = { fun_count : int } [@@deriving show]
 
 (** Converts a global id to its corresponding function id.
     To do so, it adds the global id to the number of function declarations :
-    We have the bijection `global_fun_id <=> global_id + fun_id_count`.
+    We have the bijection [global_fun_id <=> global_id + fun_id_count].
 *)
 let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) :
     A.FunDeclId.id =
@@ -896,7 +896,7 @@ let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
          * between the globals themselves and their bodies, which are simply
          * functions with no arguments. We add the global bodies to the list
          * of function declarations: the (fresh) ids we use for those bodies
-         * are simply given by: `num_functions + global_id` *)
+         * are simply given by: [num_functions + global_id] *)
         let gid_conv = { fun_count = List.length functions } in
         let* globals =
           list_of_json
diff --git a/src/Logging.ml b/src/Logging.ml
index 6dca854c..e83f25f8 100644
--- a/src/Logging.ml
+++ b/src/Logging.ml
@@ -138,7 +138,8 @@ let level_to_color (lvl : L.level) =
   | NoLevel -> Default
 
 (** [format styles str] formats [str] to the given [styles] -
-    TODO: comes from easy_logging (did not manage to reuse the module directl)
+    TODO: comes from {{: http://ocamlverse.net/content/documentation_guidelines.html}[easy_logging]}
+    (did not manage to reuse the module directly)
 *)
 let rec format styles str =
   match styles with
@@ -147,7 +148,8 @@ let rec format styles str =
       Printf.sprintf "\027[%dm%s\027[%dm" set (format styles' str) reset
   | [] -> str
 
-(** TODO: comes from easy_logging (did not manage to reuse the module directly) *)
+(** TODO: comes from {{: http://ocamlverse.net/content/documentation_guidelines.html}[easy_logging]}
+    (did not manage to reuse the module directly) *)
 let format_tags (tags : string list) =
   match tags with
   | [] -> ""
diff --git a/src/Meta.ml b/src/Meta.ml
index cca6f047..f0e4ca04 100644
--- a/src/Meta.ml
+++ b/src/Meta.ml
@@ -26,17 +26,17 @@ type meta = {
           to the macro).
 
           Ex:
-          ```text
-          // Below, we consider the spans for the statements inside `test`
+          {[
+            // Below, we consider the spans for the statements inside `test`
 
-          //   the statement we consider, which gets inlined in `test`
-                                   VV
-          macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
+            //   the statement we consider, which gets inlined in `test`
+                                     VV
+            macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
 
-          fn test() {
-              macro!(); // <-- `span` refers to this location
-          }
-          ```
+            fn test() {
+                macro!(); // <-- `span` refers to this location
+            }
+          ]}
        *)
   generated_from_span : span option;
       (** Where the code actually comes from, in case of macro expansion/inlining/etc. *)
diff --git a/src/Names.ml b/src/Names.ml
index 209f8547..a27db161 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -5,28 +5,27 @@ module Disambiguator = IdGen ()
 type path_elem = Ident of string | Disambiguator of Disambiguator.id
 [@@deriving show, ord]
 
-type name = path_elem list [@@deriving show, ord]
-(** A name such as: `std::collections::vector` (which would be represented as
+(** A name such as: [std::collections::vector] (which would be represented as
     [[Ident "std"; Ident "collections"; Ident "vector"]])
 
 
     A name really is a list of strings. However, we sometimes need to
     introduce unique indices to disambiguate. This mostly happens because
     of "impl" blocks in Rust:
-      ```
+    {[
       impl<T> List<T> {
         ...
       }
-      ```
+    ]}
    
     A type in Rust can have several "impl" blocks, and those blocks can
     contain items with similar names. For this reason, we need to disambiguate
     them with unique indices. Rustc calls those "disambiguators". In rustc, this
     gives names like this:
-    - `betree_main::betree::NodeIdCounter{impl#0}::new`
+    - [betree_main::betree::NodeIdCounter{impl#0}::new]
     - note that impl blocks can be nested, and macros sometimes generate
       weird names (which require disambiguation):
-      `betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}`
+      [betree_main::betree_utils::_#1::{impl#0}::deserialize::{impl#0}]
    
     Finally, the paths used by rustc are a lot more precise and explicit than
     those we expose in LLBC: for instance, every identifier belongs to a specific
@@ -39,11 +38,12 @@ type name = path_elem list [@@deriving show, ord]
     in the other situations (i.e., the disambiguator is always equal to 0).
    
     Moreover, the items are uniquely disambiguated by their (integer) ids
-    (`TypeDeclId.id`, etc.), and when extracting the code we have to deal with
+    ([TypeDeclId.id], etc.), and when extracting the code we have to deal with
     name clashes anyway. Still, we might want to be more precise in the future.
    
     Also note that the first path element in the name is always the crate name.
  *)
+type name = path_elem list [@@deriving show, ord]
 
 let to_name (ls : string list) : name = List.map (fun s -> Ident s) ls
 
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index cd14c398..a09ae476 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -14,13 +14,13 @@ let log = L.pre_passes_log
 (** Rustc inserts a lot of drops before the assignments.
     We consider those drops are part of the assignment, and splitting the
     drop and the assignment is problematic for us because it can introduce
-    ⊥ under borrows. For instance, we encountered situations like the
+    [⊥] under borrows. For instance, we encountered situations like the
     following one:
     
-    ```
-    drop( *x ); // Illegal! Inserts a ⊥ under a borrow
-    *x = move ...;
-    ```
+    {[
+      drop( *x ); // Illegal! Inserts a ⊥ under a borrow
+      *x = move ...;
+    ]}
 
     TODO: this is not necessary anymore
  *)
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 0a7091f0..a9e42f6c 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -239,7 +239,7 @@ let adt_variant_to_string (fmt : value_formatter) (adt_id : type_id)
       (* Assumed type *)
       match aty with
       | State ->
-          (* The `State` type is opaque: we can't get there *)
+          (* The [State] type is opaque: we can't get there *)
           raise (Failure "Unreachable")
       | Result ->
           let variant_id = Option.get variant_id in
@@ -262,7 +262,7 @@ let adt_field_to_string (fmt : value_formatter) (adt_id : type_id)
   match adt_id with
   | Tuple ->
       raise (Failure "Unreachable")
-      (* Tuples don't use the opaque field id for the field indices, but `int` *)
+      (* Tuples don't use the opaque field id for the field indices, but [int] *)
   | AdtId def_id -> (
       (* "Regular" ADT *)
       let fields = fmt.adt_field_names def_id None in
@@ -316,7 +316,7 @@ let adt_g_value_to_string (fmt : value_formatter)
       (* Assumed type *)
       match aty with
       | State ->
-          (* The `State` type is opaque: we can't get there *)
+          (* The [State] type is opaque: we can't get there *)
           raise (Failure "Unreachable")
       | Result ->
           let variant_id = Option.get variant_id in
@@ -467,7 +467,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
 and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
     (indent_incr : string) (app : texpression) (args : texpression list) :
     string =
-  (* There are two possibilities: either the `app` is an instantiated,
+  (* There are two possibilities: either the [app] is an instantiated,
    * top-level qualifier (function, ADT constructore...), or it is a "regular"
    * expression *)
   let app, tys =
diff --git a/src/Pure.ml b/src/Pure.ml
index afda2caa..77265f75 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -13,31 +13,31 @@ module SymbolicValueId = V.SymbolicValueId
 module FunDeclId = A.FunDeclId
 module GlobalDeclId = A.GlobalDeclId
 
-module SynthPhaseId = IdGen ()
 (** We give an identifier to every phase of the synthesis (forward, backward
     for group of regions 0, etc.) *)
+module SynthPhaseId = IdGen ()
 
+(** Pay attention to the fact that we also define a {!Values.VarId} module in Values *)
 module VarId = IdGen ()
-(** Pay attention to the fact that we also define a [VarId] module in Values *)
 
 type integer_type = T.integer_type [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
     In comparison with LLBC:
-    - we removed `Box` (because it is translated as the identity: `Box T == T`)
+    - we removed [Box] (because it is translated as the identity: [Box T == T])
     - we added:
-      - `Result`: the type used in the error monad. This allows us to have a
+      - [Result]: the type used in the error monad. This allows us to have a
         unified treatment of expressions (especially when we have to unfold the
         monadic binds)
-      - `State`: the type of the state, when using state-error monads. Note that
+      - [State]: the type of the state, when using state-error monads. Note that
         this state is opaque to Aeneas (the user can define it, or leave it as
         assumed)
   *)
 type assumed_ty = State | Result | Vec | Option [@@deriving show, ord]
 
-(* TODO: we should never directly manipulate `Return` and `Fail`, but rather
- * the monadic functions `return` and `fail` (makes treatment of error and
+(* TODO: we should never directly manipulate [Return] and [Fail], but rather
+ * the monadic functions [return] and [fail] (makes treatment of error and
  * state-error monads more uniform) *)
 let result_return_id = VariantId.of_int 0
 let result_fail_id = VariantId.of_int 1
@@ -69,7 +69,7 @@ class ['self] map_ty_base =
 
 type ty =
   | Adt of type_id * ty list
-      (** [Adt] encodes ADTs and tuples and assumed types.
+      (** {!Adt} encodes ADTs and tuples and assumed types.
        
           TODO: what about the ended regions? (ADTs may be parameterized
           with several region variables. When giving back an ADT value, we may
@@ -91,7 +91,7 @@ type ty =
         name = "iter_ty";
         variety = "iter";
         ancestors = [ "iter_ty_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
       },
@@ -100,7 +100,7 @@ type ty =
         name = "map_ty";
         variety = "map";
         ancestors = [ "map_ty_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
       }]
@@ -124,6 +124,10 @@ type type_decl = {
 type scalar_value = V.scalar_value [@@deriving show]
 type constant_value = V.constant_value [@@deriving show]
 
+(** Because we introduce a lot of temporary variables, the list of variables
+    is not fixed: we thus must carry all its information with the variable
+    itself.
+ *)
 type var = {
   id : VarId.id;
   basename : string option;
@@ -133,10 +137,6 @@ type var = {
   ty : ty;
 }
 [@@deriving show]
-(** Because we introduce a lot of temporary variables, the list of variables
-    is not fixed: we thus must carry all its information with the variable
-    itself.
- *)
 
 (* TODO: we might want to redefine field_proj_kind here, to prevent field accesses
  * on enumerations.
@@ -148,18 +148,18 @@ type mprojection_elem = { pkind : E.field_proj_kind; field_id : FieldId.id }
 
 type mprojection = mprojection_elem list [@@deriving show]
 
-type mplace = {
-  var_id : V.VarId.id;
-  name : string option;
-  projection : mprojection;
-}
-[@@deriving show]
 (** "Meta" place.
 
     Meta-data retrieved from the symbolic execution, which gives provenance
     information about the values. We use this to generate names for the variables
     we introduce.
  *)
+type mplace = {
+  var_id : V.VarId.id;
+  name : string option;
+  projection : mprojection;
+}
+[@@deriving show]
 
 type variant_id = VariantId.id [@@deriving show]
 
@@ -225,10 +225,10 @@ class virtual ['self] mapreduce_value_base =
 (** A pattern (which appears on the left of assignments, in matches, etc.). *)
 type pattern =
   | PatConcrete of constant_value
-      (** [PatConcrete] is necessary because we merge the switches over integer
+      (** {!PatConcrete} is necessary because we merge the switches over integer
           values and the matches over enumerations *)
   | PatVar of var * mplace option
-  | PatDummy  (** Ignored value: `_`. *)
+  | PatDummy  (** Ignored value: [_]. *)
   | PatAdt of adt_pattern
 
 and adt_pattern = {
@@ -244,7 +244,7 @@ and typed_pattern = { value : pattern; ty : ty }
         name = "iter_typed_pattern";
         variety = "iter";
         ancestors = [ "iter_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
       },
@@ -253,7 +253,7 @@ and typed_pattern = { value : pattern; ty : ty }
         name = "map_typed_pattern";
         variety = "map";
         ancestors = [ "map_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
       },
@@ -262,7 +262,7 @@ and typed_pattern = { value : pattern; ty : ty }
         name = "reduce_typed_pattern";
         variety = "reduce";
         ancestors = [ "reduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         polymorphic = false;
       },
     visitors
@@ -270,7 +270,7 @@ and typed_pattern = { value : pattern; ty : ty }
         name = "mapreduce_typed_pattern";
         variety = "mapreduce";
         ancestors = [ "mapreduce_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         polymorphic = false;
       }]
 
@@ -279,28 +279,28 @@ type unop = Not | Neg of integer_type | Cast of integer_type * integer_type
 
 type fun_id =
   | Regular of A.fun_id * T.RegionGroupId.id option
-      (** Backward id: `Some` if the function is a backward function, `None`
+      (** Backward id: [Some] if the function is a backward function, [None]
           if it is a forward function.
 
-          TODO: we need to redefine A.fun_id here, to add `fail` and
-          `return` (important to get a unified treatment of the state-error
+          TODO: we need to redefine A.fun_id here, to add [fail] and
+          [return] (important to get a unified treatment of the state-error
           monad). For now, when using the state-error monad: extraction
           works only if we unfold all the monadic let-bindings, and we
-          then replace the content of the occurrences of `Return` to also
+          then replace the content of the occurrences of [Return] to also
           return the state (which is really super ugly).
        *)
   | Unop of unop
   | Binop of E.binop * integer_type
 [@@deriving show, ord]
 
+(** An identifier for an ADT constructor *)
 type adt_cons_id = { adt_id : type_id; variant_id : variant_id option }
 [@@deriving show]
-(** An identifier for an ADT constructor *)
 
-type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
 (** Projection - For now we don't support projection of tuple fields 
     (because not all the backends have syntax for this).
  *)
+type projection = { adt_id : type_id; field_id : FieldId.id } [@@deriving show]
 
 type qualif_id =
   | Func of fun_id
@@ -309,13 +309,13 @@ type qualif_id =
   | Proj of projection  (** Field projector *)
 [@@deriving show]
 
-type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
 (** An instantiated qualified.
 
     Note that for now we have a clear separation between types and expressions,
-    which explains why we have the `type_params` field: a function or ADT
+    which explains why we have the [type_params] field: a function or ADT
     constructor is always fully instantiated.
  *)
+type qualif = { id : qualif_id; type_args : ty list } [@@deriving show]
 
 type var_id = VarId.id [@@deriving show]
 
@@ -367,7 +367,7 @@ class virtual ['self] mapreduce_expression_base =
       fun _ x -> (x, self#zero)
   end
 
-(** **Rk.:** here, [expression] is not at all equivalent to the expressions
+(** **Rk.:** here, {!expression} is not at all equivalent to the expressions
     used in LLBC. They are lambda-calculus expressions, and are thus actually
     more general than the LLBC statements, in a sense.
  *)
@@ -383,7 +383,7 @@ type expression =
           field accesses with calls to projectors over fields (when there
           are clashes of field names, some provers like F* get pretty bad...)
        *)
-  | Abs of typed_pattern * texpression  (** Lambda abstraction: `fun x -> e` *)
+  | Abs of typed_pattern * texpression  (** Lambda abstraction: [fun x -> e] *)
   | Qualif of qualif  (** A top-level qualifier *)
   | Let of bool * typed_pattern * texpression * texpression
       (** Let binding.
@@ -395,34 +395,33 @@ type expression =
 
           The boolean controls whether the let is monadic or not.
           For instance, in F*:
-          - non-monadic: `let x = ... in ...`
-          - monadic:     `x <-- ...; ...`
+          - non-monadic: [let x = ... in ...]
+          - monadic:     [x <-- ...; ...]
 
           Note that we are quite general for the left-value on purpose; this
           is used in several situations:
 
           1. When deconstructing a tuple:
-          ```
-          let (x, y) = p in ...
-          ```
-          (not all languages have syntax like `p.0`, `p.1`... and it is more
+          {[
+            let (x, y) = p in ...
+          ]}
+          (not all languages have syntax like [p.0], [p.1]... and it is more
           readable anyway).
           
           2. When expanding an enumeration with one variant.
-          
-          In this case, [Deconstruct] has to be understood as:
-          ```
-          let Cons x tl = ls in
-          ...
-          ```
+          In this case, {!Let} has to be understood as:
+          {[
+            let Cons x tl = ls in
+            ...
+          ]}
           
           Note that later, depending on the language we extract to, we can
           eventually update it to something like this (for F*, for instance):
-          ```
-          let x = Cons?.v ls in
-          let tl = Cons?.tl ls in
-          ...
-          ```
+          {[
+            let x = Cons?.v ls in
+            let tl = Cons?.tl ls in
+            ...
+          ]}
        *)
   | Switch of texpression * switch_body
   | Meta of (meta[@opaque]) * texpression  (** Meta-information *)
@@ -431,12 +430,12 @@ and switch_body = If of texpression * texpression | Match of match_branch list
 and match_branch = { pat : typed_pattern; branch : texpression }
 and texpression = { e : expression; ty : ty }
 
-and mvalue = (texpression[@opaque])
 (** Meta-value (converted to an expression). It is important that the content
     is opaque.
     
     TODO: is it possible to mark the whole mvalue type as opaque?
  *)
+and mvalue = (texpression[@opaque])
 
 and meta =
   | Assignment of mplace * mvalue * mplace option
@@ -454,7 +453,7 @@ and meta =
         name = "iter_expression";
         variety = "iter";
         ancestors = [ "iter_expression_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -462,7 +461,7 @@ and meta =
         name = "map_expression";
         variety = "map";
         ancestors = [ "map_expression_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -470,25 +469,26 @@ and meta =
         name = "reduce_expression";
         variety = "reduce";
         ancestors = [ "reduce_expression_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
       },
     visitors
       {
         name = "mapreduce_expression";
         variety = "mapreduce";
         ancestors = [ "mapreduce_expression_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
       }]
 
+(** Information about the "effect" of a function *)
 type fun_effect_info = {
-  input_state : bool;  (** `true` if the function takes a state as input *)
+  input_state : bool;  (** [true] if the function takes a state as input *)
   output_state : bool;
-      (** `true` if the function outputs a state (it then lives
+      (** [true] if the function outputs a state (it then lives
                             in a state monad) *)
-  can_fail : bool;  (** `true` if the return type is a `result` *)
+  can_fail : bool;  (** [true] if the return type is a [result] *)
 }
-(** Information about the "effect" of a function *)
 
+(** Meta information about a function signature *)
 type fun_sig_info = {
   num_fwd_inputs : int;
       (** The number of input types for forward computation *)
@@ -496,38 +496,12 @@ type fun_sig_info = {
       (** The number of additional inputs for the backward computation (if pertinent) *)
   effect_info : fun_effect_info;
 }
-(** Meta information about a function signature *)
 
-type fun_sig = {
-  type_params : type_var list;
-  inputs : ty list;
-  output : ty;
-  doutputs : ty list;
-      (** The "decomposed" list of outputs.
-
-          In case of a forward function, the list has length = 1, for the
-          type of the returned value.
-          
-          In case of backward function, the list contains all the types of
-          all the given back values (there is at most one type per forward
-          input argument).
-          
-          Ex.:
-          ```
-          fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
-          ```
-          Decomposed outputs:
-          - forward function:  [T]
-          - backward function: [T; T] (for "x" and "y")
-          
-       *)
-  info : fun_sig_info;  (** Additional information *)
-}
 (** A function signature.
 
     We have the following cases:
     - forward function:
-      `in_ty0 -> ... -> in_tyn -> out_ty`                           (* pure function *)
+      [in_ty0 -> ... -> in_tyn -> out_ty]                           (* pure function *)
       `in_ty0 -> ... -> in_tyn -> result out_ty`                    (* error-monad *)
       `in_ty0 -> ... -> in_tyn -> state -> result (state & out_ty)` (* state-error *)
     - backward function:
@@ -550,20 +524,45 @@ type fun_sig = {
       input, or can fail, etc. without having to inspect the signature
     - etc.
  *)
+type fun_sig = {
+  type_params : type_var list;
+  inputs : ty list;
+  output : ty;
+  doutputs : ty list;
+      (** The "decomposed" list of outputs.
+
+          In case of a forward function, the list has length = 1, for the
+          type of the returned value.
+          
+          In case of backward function, the list contains all the types of
+          all the given back values (there is at most one type per forward
+          input argument).
+          
+          Ex.:
+          {[
+            fn choose<'a, T>(b : bool, x : &'a mut T, y : &'a mut T) -> &'a mut T;
+          ]}
+          Decomposed outputs:
+          - forward function:  [T]
+          - backward function: [T; T] (for "x" and "y")
+          
+       *)
+  info : fun_sig_info;  (** Additional information *)
+}
 
+(** An instantiated function signature. See {!fun_sig} *)
 type inst_fun_sig = {
   inputs : ty list;
   output : ty;
   doutputs : ty list;
   info : fun_sig_info;
 }
-(** An instantiated function signature. See [fun_sig] *)
 
 type fun_body = {
   inputs : var list;
   inputs_lvs : typed_pattern list;
       (** The inputs seen as patterns. Allows to make transformations, for example
-          to replace unused variables by `_` *)
+          to replace unused variables by [_] *)
   body : texpression;
 }
 
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index c8ebfa6b..3edae38a 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -8,51 +8,52 @@ module V = Values
 (** The local logger *)
 let log = L.pure_micro_passes_log
 
+(** A configuration to control the application of the passes *)
 type config = {
   decompose_monadic_let_bindings : bool;
       (** Some provers like F* don't support the decomposition of return values
           in monadic let-bindings:
-          ```
-          // NOT supported in F*
-          let (x, y) <-- f ();
-          ...
-          ```
+          {[
+            // NOT supported in F*
+            let (x, y) <-- f ();
+            ...
+          ]}
 
           In such situations, we might want to introduce an intermediate
           assignment:
-          ```
-          let tmp <-- f ();
-          let (x, y) = tmp in
-          ...
-          ```
+          {[
+            let tmp <-- f ();
+            let (x, y) = tmp in
+            ...
+          ]}
        *)
   unfold_monadic_let_bindings : bool;
       (** Controls the unfolding of monadic let-bindings to explicit matches:
           
-          `y <-- f x; ...`
+          [y <-- f x; ...]
 
           becomes:
           
-          `match f x with | Failure -> Failure | Return y -> ...`
+          [match f x with | Failure -> Failure | Return y -> ...]
 
           
           This is useful when extracting to F*: the support for monadic
           definitions is not super powerful.
-          Note that when [undolf_monadic_let_bindings] is true, setting
-          [decompose_monadic_let_bindings] to true and only makes the code
+          Note that when {!field:unfold_monadic_let_bindings} is true, setting
+          {!field:decompose_monadic_let_bindings} to true and only makes the code
           more verbose.
        *)
   filter_useless_monadic_calls : bool;
       (** Controls whether we try to filter the calls to monadic functions
           (which can fail) when their outputs are not used.
           
-          See the comments for [expression_contains_child_call_in_all_paths]
+          See the comments for {!expression_contains_child_call_in_all_paths}
           for additional explanations.
           
-          TODO: rename to [filter_useless_monadic_calls]
+          TODO: rename to {!filter_useless_monadic_calls}
        *)
   filter_useless_functions : bool;
-      (** If [filter_useless_monadic_calls] is activated, some functions
+      (** If {!filter_useless_monadic_calls} is activated, some functions
           become useless: if this option is true, we don't extract them.
 
           The calls to functions which always get filtered are:
@@ -64,7 +65,6 @@ type config = {
             dynamically check for that).
        *)
 }
-(** A configuration to control the application of the passes *)
 
 (** Small utility.
 
@@ -89,24 +89,24 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
       method plus id0 id1 _ = VarId.max (id0 ()) (id1 ())
       (* Get the maximum *)
 
-      method! visit_var _ v _ = v.id
       (** For the patterns *)
+      method! visit_var _ v _ = v.id
 
-      method! visit_Var _ vid _ = vid
       (** For the rvalues *)
+      method! visit_Var _ vid _ = vid
     end
   in
   (* Find the max counter in the body *)
   let id = obj#visit_expression () body.body.e () in
   VarId.generator_from_incr_id id
 
+(** "pretty-name context": see [compute_pretty_names] *)
 type pn_ctx = {
   pure_vars : string VarId.Map.t;
       (** Information about the pure variables used in the synthesized program *)
   llbc_vars : string V.VarId.Map.t;
       (** Information about the LLBC variables used in the original program *)
 }
-(** "pretty-name context": see [compute_pretty_names] *)
 
 (** This function computes pretty names for the variables in the pure AST. It
     relies on the "meta"-place information in the AST to generate naming
@@ -128,49 +128,49 @@ type pn_ctx = {
     For instance, the following situations happen:
     
     - let's say we evaluate:
-      ```
-      match (ls : List<T>) {
-        List::Cons(x, hd) => {
-          ...
+      {[
+        match (ls : List<T>) {
+          List::Cons(x, hd) => {
+            ...
+          }
         }
-      }
-      ```
+      ]}
       
       Actually, in MIR, we get:
-      ```
-      tmp := discriminant(ls);
-      switch tmp {
-        0 => {
-          x := (ls as Cons).0; // (i)
-          hd := (ls as Cons).1; // (ii)
-          ...
+      {[
+        tmp := discriminant(ls);
+        switch tmp {
+          0 => {
+            x := (ls as Cons).0; // (i)
+            hd := (ls as Cons).1; // (ii)
+            ...
+          }
         }
-      }
-      ```
-      If `ls` maps to a symbolic value `s0` upon evaluating the match in symbolic
-      mode, we expand this value upon evaluating `tmp = discriminant(ls)`.
+      ]}
+      If [ls] maps to a symbolic value [s0] upon evaluating the match in symbolic
+      mode, we expand this value upon evaluating [tmp = discriminant(ls)].
       However, at this point, we don't know which should be the names of
-      the symbolic values we introduce for the fields of `Cons`!
+      the symbolic values we introduce for the fields of [Cons]!
 
-      Let's imagine we have (for the `Cons` branch): `s0 ~~> Cons s1 s2`.
+      Let's imagine we have (for the [Cons] branch): [s0 ~~> Cons s1 s2].
       The assigments at (i) and (ii) lead to the following binding in the
       evaluation context:
-      ```
-      x -> s1
-      hd -> s2
-      ```
+      {[
+        x -> s1
+        hd -> s2
+      ]}
       
       When generating the symbolic AST, we save as meta-information that we
-      assign `s1` to the place `x` and `s2` to the place `hd`. This way,
-      we learn we can use the names `x` and `hd` for the variables which are
+      assign [s1] to the place [x] and [s2] to the place [hd]. This way,
+      we learn we can use the names [x] and [hd] for the variables which are
       introduced by the match:
-      ```
-      match ls with
-      | Cons x hd -> ...
-      | ...
-      ```
+      {[
+        match ls with
+        | Cons x hd -> ...
+        | ...
+      ]}
    - Assignments:
-     `let x [@mplace=lp] = v [@mplace = rp} in ...`
+     [let x [@mplace=lp] = v [@mplace = rp] in ...]
      
      We propagate naming information across the assignments. This is important
      because many reassignments using temporary, anonymous variables are
@@ -178,39 +178,39 @@ type pn_ctx = {
    
    - Given back values (introduced by backward functions):
      Let's say we have the following Rust code:
-     ```
-     let py = id(&mut x);
-     *py = 2;
-     assert!(x == 2);
-     ```
+     {[
+       let py = id(&mut x);
+       *py = 2;
+       assert!(x == 2);
+     ]}
      
      After desugaring, we get the following MIR:
-     ```
-     ^0 = &mut x; // anonymous variable
-     py = id(move ^0);
-     *py += 2;
-     assert!(x == 2);
-     ```
+     {[
+       ^0 = &mut x; // anonymous variable
+       py = id(move ^0);
+       *py += 2;
+       assert!(x == 2);
+     ]}
      
      We want this to be translated as:
-     ```
-     let py = id_fwd x in
-     let py1 = py + 2 in
-     let x1 = id_back x py1 in // <-- x1 is "given back": doesn't appear in the original MIR
-     assert(x1 = 2);
-     ```
-
-     We want to notice that the value given back by `id_back` is given back for "x",
+     {[
+       let py = id_fwd x in
+       let py1 = py + 2 in
+       let x1 = id_back x py1 in // <-- x1 is "given back": doesn't appear in the original MIR
+       assert(x1 = 2);
+     ]}
+
+     We want to notice that the value given back by [id_back] is given back for "x",
      so we should use "x" as the basename (hence the resulting name "x1"). However,
-     this is non-trivial, because after desugaring the input argument given to `id`
-     is not `&mut x` but `move ^0` (i.e., it comes from a temporary, anonymous
-     variable). For this reason, we use the meta-place "&mut x" as the meta-place
+     this is non-trivial, because after desugaring the input argument given to [id]
+     is not [&mut x] but [move ^0] (i.e., it comes from a temporary, anonymous
+     variable). For this reason, we use the meta-place [&mut x] as the meta-place
      for the given back value (this is done during the synthesis), and propagate
      naming information *also* on the LLBC variables (which are referenced by the
      meta-places).
 
-     This way, because of `^0 = &mut x`, we can propagate the name "x" to the place
-     `^0`, then to the given back variable across the function call.
+     This way, because of [^0 = &mut x], we can propagate the name "x" to the place
+     [^0], then to the given back variable across the function call.
    
  *)
 let compute_pretty_names (def : fun_decl) : fun_decl =
@@ -372,7 +372,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
    * rvalue to the left *)
   let add_left_right_constraint (lv : typed_pattern) (re : texpression)
       (ctx : pn_ctx) : pn_ctx =
-    (* We propagate constraints across variable reassignments: `^0 = x`,
+    (* We propagate constraints across variable reassignments: [^0 = x],
      * if the destination doesn't have naming information *)
     match lv.value with
     | PatVar (({ id = _; basename = None; ty = _ } as lvar), lmp) ->
@@ -552,17 +552,17 @@ let remove_meta (def : fun_decl) : fun_decl =
     compilation to MIR and by the translation itself (and the variable used
     on the left is often unnamed).
 
-    Note that many of them are just variable "reassignments": `let x = y in ...`.
+    Note that many of them are just variable "reassignments": [let x = y in ...].
     Some others come from ??
     
     TODO: how do we call that when we introduce intermediate variable assignments
     for the arguments of a function call?
 
-    [inline_named]: if `true`, inline all the assignments of the form
-    `let VAR = VAR in ...`, otherwise inline only the ones where the variable
+    [inline_named]: if [true], inline all the assignments of the form
+    [let VAR = VAR in ...], otherwise inline only the ones where the variable
     on the left is anonymous.
     
-    [inline_pure]: if `true`, inline all the pure assignments where the variable
+    [inline_pure]: if [true], inline all the pure assignments where the variable
     on the left is anonymous, but the assignments where the r-expression is
     a non-primitive function call (i.e.: inline the binops, ADT constructions,
     etc.).
@@ -578,6 +578,8 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
     object (self)
       inherit [_] map_expression as super
 
+      (** Visit the let-bindings to filter the useless ones (and update
+          the substitution map while doing so *)
       method! visit_Let (env : texpression VarId.Map.t) monadic lv re e =
         (* In order to filter, we need to check first that:
          * - the let-binding is not monadic
@@ -598,7 +600,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
             (* Or:
              * 2.2 the right-expression is a constant value, an ADT value,
              *     a projection or a primitive function call *and* the flag
-             *     `inline_pure` is set *)
+             *     [inline_pure] is set *)
             let pure_re =
               is_const re
               ||
@@ -625,12 +627,11 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
             let env = if filter then VarId.Map.add lv_var.id re env else env in
             (* Update the next expression *)
             let e = self#visit_texpression env e in
-            (* Reconstruct the `let`, only if the binding is not filtered *)
+            (* Reconstruct the [let], only if the binding is not filtered *)
             if filter then e.e else Let (monadic, lv, re, e)
         | _ -> super#visit_Let env monadic lv re e
-      (** Visit the let-bindings to filter the useless ones (and update
-          the substitution map while doing so *)
 
+      (** Substitute the variables *)
       method! visit_Var (env : texpression VarId.Map.t) (vid : VarId.id) =
         match VarId.Map.find_opt vid env with
         | None -> (* No substitution *) super#visit_Var env vid
@@ -641,7 +642,6 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
              * var1 --> var2.
              *)
             self#visit_expression env ne.e
-      (** Substitute the variables *)
     end
   in
   match def.body with
@@ -663,19 +663,19 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
     the additional inputs those receive).
     
     For instance, if we have:
-    ```
-    fn f<'a>(x : &'a mut T);
-    ```
+    {[
+      fn f<'a>(x : &'a mut T);
+    ]}
     
     We often have  things like this in the synthesized code:
-    ```
-    _ <-- f x;
-    ...
-    nx <-- f@back'a x y;
-    ...
-    ```
-
-    In this situation, we can remove the call `f x`.
+    {[
+      _ <-- f x;
+      ...
+      nx <-- f@back'a x y;
+      ...
+    ]}
+
+    In this situation, we can remove the call [f x].
  *)
 let expression_contains_child_call_in_all_paths (ctx : trans_ctx)
     (fun_id0 : fun_id) (tys0 : ty list) (args0 : texpression list)
@@ -785,14 +785,14 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
     (def : fun_decl) : fun_decl =
   (* We first need a transformation on *left-values*, which filters the useless
    * variables and tells us whether the value contains any variable which has
-   * not been replaced by `_` (in which case we need to keep the assignment,
+   * not been replaced by [_] (in which case we need to keep the assignment,
    * etc.).
    * 
    * This is implemented as a map-reduce.
    *
    * Returns: ( filtered_left_value, *all_dummies* )
    *
-   * `all_dummies`:
+   * [all_dummies]:
    * If the returned boolean is true, it means that all the variables appearing
    * in the filtered left-value are *dummies* (meaning that if this left-value
    * appears at the left of a let-binding, this binding might potentially be
@@ -826,8 +826,8 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
       method zero _ = VarId.Set.empty
       method plus s0 s1 _ = VarId.Set.union (s0 ()) (s1 ())
 
-      method! visit_Var _ vid = (Var vid, fun _ -> VarId.Set.singleton vid)
       (** Whenever we visit a variable, we need to register the used variable *)
+      method! visit_Var _ vid = (Var vid, fun _ -> VarId.Set.singleton vid)
 
       method! visit_expression env e =
         match e with
@@ -903,13 +903,13 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx)
 
 (** Simplify the aggregated ADTs.
     Ex.:
-    ```
-    type struct = { f0 : nat; f1 : nat }
-    
-    Mkstruct x.f0 x.f1 ~~> x
-    ```
+    {[
+      type struct = { f0 : nat; f1 : nat }
+
+      Mkstruct x.f0 x.f1 ~~> x
+    ]}
     
-    TODO: introduce a notation for { x with field = ... }, and use it.
+    TODO: introduce a notation for [{ x with field = ... }], and use it.
  *)
 let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
   let expr_visitor =
@@ -943,7 +943,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
                 assert (num_fields > 0);
                 if num_fields = List.length args then
                   (* We now need to check that all the arguments are of the form:
-                   * `x.field` for some variable `x`, and where the projection
+                   * [x.field] for some variable [x], and where the projection
                    * is for the proper ADT *)
                   let to_var_proj (i : int) (arg : texpression) :
                       (ty list * var_id) option =
@@ -995,7 +995,7 @@ let simplify_aggregates (ctx : trans_ctx) (def : fun_decl) : fun_decl =
       let body = { body with body = body_exp } in
       { def with body = Some body }
 
-(** Return `None` if the function is a backward function with no outputs (so
+(** Return [None] if the function is a backward function with no outputs (so
     that we eliminate the definition which is useless).
 
     Note that the calls to such functions are filtered when translating from
@@ -1010,7 +1010,7 @@ let filter_if_backward_with_no_outputs (config : config) (def : fun_decl) :
   then None
   else Some def
 
-(** Return `false` if the forward function is useless and should be filtered.
+(** Return [false] if the forward function is useless and should be filtered.
 
     - a forward function with no output (comes from a Rust function with
       unit return type)
@@ -1037,24 +1037,24 @@ let keep_forward (config : config) (trans : pure_fun_translation) : bool =
   then false
   else true
 
-(** Convert the unit variables to `()` if they are used as right-values or
-    `_` if they are used as left values in patterns. *)
+(** Convert the unit variables to [()] if they are used as right-values or
+    [_] if they are used as left values in patterns. *)
 let unit_vars_to_unit (def : fun_decl) : fun_decl =
   (* The map visitor *)
   let obj =
     object
       inherit [_] map_expression as super
 
+      (** Replace in patterns *)
       method! visit_PatVar _ v mp =
         if v.ty = mk_unit_ty then PatDummy else PatVar (v, mp)
-      (** Replace in patterns *)
 
-      method! visit_texpression env e =
-        if e.ty = mk_unit_ty then mk_unit_rvalue
-        else super#visit_texpression env e
       (** Replace in "regular" expressions - note that we could limit ourselves
           to variables, but this is more powerful
        *)
+      method! visit_texpression env e =
+        if e.ty = mk_unit_ty then mk_unit_rvalue
+        else super#visit_texpression env e
     end
   in
   (* Update the body *)
@@ -1068,8 +1068,8 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl =
       let body = Some { body with body = body_exp; inputs_lvs } in
       { def with body }
 
-(** Eliminate the box functions like `Box::new`, `Box::deref`, etc. Most of them
-    are translated to identity, and `Box::free` is translated to `()`.
+(** Eliminate the box functions like [Box::new], [Box::deref], etc. Most of them
+    are translated to identity, and [Box::free] is translated to [()].
 
     Note that the box types have already been eliminated during the translation
     from symbolic to pure.
@@ -1091,7 +1091,7 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
             | Regular (A.Assumed aid, rg_id) -> (
                 (* Below, when dealing with the arguments: we consider the very
                  * general case, where functions could be boxed (meaning we
-                 * could have: `box_new f x`)
+                 * could have: [box_new f x])
                  * *)
                 match (aid, rg_id) with
                 | A.BoxNew, _ ->
@@ -1099,19 +1099,19 @@ let eliminate_box_functions (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
                 | A.BoxDeref, None ->
-                    (* `Box::deref` forward is the identity *)
+                    (* [Box::deref] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
                 | A.BoxDeref, Some _ ->
-                    (* `Box::deref` backward is `()` (doesn't give back anything) *)
+                    (* [Box::deref] backward is [()] (doesn't give back anything) *)
                     assert (args = []);
                     mk_unit_rvalue
                 | A.BoxDerefMut, None ->
-                    (* `Box::deref_mut` forward is the identity *)
+                    (* [Box::deref_mut] forward is the identity *)
                     let arg, args = Collections.List.pop args in
                     mk_apps arg args
                 | A.BoxDerefMut, Some _ ->
-                    (* `Box::deref_mut` back is almost the identity:
+                    (* [Box::deref_mut] back is almost the identity:
                      * let box_deref_mut (x_init : t) (x_back : t) : t = x_back
                      * *)
                     let arg, args =
@@ -1197,24 +1197,24 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
 
           method! visit_Let env monadic lv re e =
             (* We simply do the following transformation:
-             * ```
-             * pat <-- re; e
-             *
-             *     ~~>
-             *
-             * match re with
-             * | Fail err -> Fail err
-             * | Return pat -> e
-             * ```
-             *)
+               {[
+                 pat <-- re; e
+
+                     ~~>
+
+                 match re with
+                 | Fail err -> Fail err
+                 | Return pat -> e
+               ]}
+            *)
             (* TODO: we should use a monad "kind" instead of a boolean *)
             if not monadic then super#visit_Let env monadic lv re e
             else
               (* We don't do the same thing if we use a state-error monad or simply
-               * an error monad.
-               * Note that some functions always live in the error monad (arithmetic
-               * operations, for instance).
-               *)
+                 an error monad.
+                 Note that some functions always live in the error monad (arithmetic
+                 operations, for instance).
+              *)
               (* TODO: this information should be computed in SymbolicToPure and
                * store in an enum ("monadic" should be an enum, not a bool). *)
               let re_ty = Option.get (opt_destruct_result re.ty) in
@@ -1238,7 +1238,7 @@ let unfold_monadic_let_bindings (_ctx : trans_ctx) (def : fun_decl) : fun_decl =
 
 (** Apply all the micro-passes to a function.
 
-    Will return `None` if the function is a backward function with no outputs.
+    Will return [None] if the function is a backward function with no outputs.
 
     [ctx]: used only for printing.
  *)
@@ -1278,8 +1278,8 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
   match def with
   | None -> None
   | Some def ->
-      (* Convert the unit variables to `()` if they are used as right-values or
-       * `_` if they are used as left values. *)
+      (* Convert the unit variables to [()] if they are used as right-values or
+       * [_] if they are used as left values. *)
       let def = unit_vars_to_unit def in
       log#ldebug
         (lazy ("unit_vars_to_unit:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
@@ -1308,13 +1308,13 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
         (lazy ("filter_useless:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
 
       (* Simplify the aggregated ADTs.
-       * Ex.:
-       * ```
-       * type struct = { f0 : nat; f1 : nat }
-       * 
-       * Mkstruct x.f0 x.f1 ~~> x
-       * ```
-       *)
+         Ex.:
+         {[
+           type struct = { f0 : nat; f1 : nat }
+
+           Mkstruct x.f0 x.f1 ~~> x
+         ]}
+      *)
       let def = simplify_aggregates ctx def in
       log#ldebug
         (lazy ("simplify_aggregates:\n\n" ^ fun_decl_to_string ctx def ^ "\n"));
@@ -1358,7 +1358,7 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_decl) :
 (** Return the forward/backward translations on which we applied the micro-passes.
 
     Also returns a boolean indicating whether the forward function should be kept
-    or not (because useful/useless - `true` means we need to keep the forward
+    or not (because useful/useless - [true] means we need to keep the forward
     function).
     Note that we don't "filter" the forward function and return a boolean instead,
     because this function contains useful information to extract the backward
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index 07a1732c..77c3afd4 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -34,6 +34,18 @@ type global_name = Names.global_name
 type fun_name = Names.fun_name
 
 (* TODO: this should a module we give to a functor! *)
+
+(** A formatter's role is twofold:
+    1. Come up with name suggestions.
+    For instance, provided some information about a function (its basename,
+    information about the region group, etc.) it should come up with an
+    appropriate name for the forward/backward function.
+    
+    It can of course apply many transformations, like changing to camel case/
+    snake case, adding prefixes/suffixes, etc.
+    
+    2. Format some specific terms, like constants.
+ *)
 type formatter = {
   bool_name : string;
   char_name : string;
@@ -49,7 +61,7 @@ type formatter = {
           generate some names if we want to extract the structures to records...
           We might want to extract such structures to tuples, later, but field
           access then causes trouble because not all provers accept syntax like
-          `x.3` where `x` is a tuple.
+          [x.3] where [x] is a tuple.
        *)
   variant_name : name -> string -> string;
       (** Inputs:
@@ -60,10 +72,10 @@ type formatter = {
       (** Structure constructors are used when constructing structure values.
       
           For instance, in F*:
-          ```
-          type pair = { x : nat; y : nat }
-          let p : pair = Mkpair 0 1
-          ```
+          {[
+            type pair = { x : nat; y : nat }
+            let p : pair = Mkpair 0 1
+          ]}
           
           Inputs:
           - type name
@@ -85,7 +97,7 @@ type formatter = {
           - function basename
           - number of region groups
           - region group information in case of a backward function
-            (`None` if forward function)
+            ([None] if forward function)
           - pair:
             - do we generate the forward function (it may have been filtered)?
             - the number of extracted backward functions (not necessarily equal
@@ -130,8 +142,9 @@ type formatter = {
       
           Inputs:
           - formatter
-          - [inside]: if `true`, the value should be wrapped in parentheses
-            if it is made of an application (ex.: `U32 3`)
+          - [inside]: if [true], the value should be wrapped in parentheses
+            if it is made of an application (ex.: [U32 3])
+          - the constant value
        *)
   extract_unop :
     (bool -> texpression -> unit) ->
@@ -143,6 +156,7 @@ type formatter = {
       (** Format a unary operation
       
           Inputs:
+          - a formatter for expressions (called on the argument of the unop)
           - extraction context (see below)
           - formatter
           - expression formatter
@@ -162,6 +176,7 @@ type formatter = {
       (** Format a binary operation
       
           Inputs:
+          - a formatter for expressions (called on the arguments of the binop)
           - extraction context (see below)
           - formatter
           - expression formatter
@@ -171,17 +186,6 @@ type formatter = {
           - argument 1
        *)
 }
-(** A formatter's role is twofold:
-    1. Come up with name suggestions.
-    For instance, provided some information about a function (its basename,
-    information about the region group, etc.) it should come up with an
-    appropriate name for the forward/backward function.
-    
-    It can of course apply many transformations, like changing to camel case/
-    snake case, adding prefixes/suffixes, etc.
-    
-    2. Format some specific terms, like constants.
- *)
 
 (** We use identifiers to look for name clashes *)
 type id =
@@ -199,10 +203,10 @@ type id =
           constructors.
           
           For instance, in F*:
-          ```
-          type pair = { x: nat; y : nat }
-          let p : pair = Mkpair 0 1
-          ```
+          {[
+            type pair = { x: nat; y : nat }
+            let p : pair = Mkpair 0 1
+          ]}
        *)
   | VariantId of type_id * VariantId.id
       (** If often happens that variant names must be unique (it is the case in
@@ -233,6 +237,12 @@ end
 
 module IdMap = Collections.MakeMap (IdOrderedType)
 
+(** The names map stores the mappings from names to identifiers and vice-versa.
+
+    We use it for lookups (during the translation) and to check for name clashes.
+    
+    [id_to_string] is for debugging.
+  *)
 type names_map = {
   id_to_name : string IdMap.t;
   name_to_id : id StringMap.t;
@@ -242,12 +252,6 @@ type names_map = {
        *)
   names_set : StringSet.t;
 }
-(** The names map stores the mappings from names to identifiers and vice-versa.
-
-    We use it for lookups (during the translation) and to check for name clashes.
-    
-    [id_to_string] is for debugging.
-  *)
 
 let names_map_add (id_to_string : id -> string) (id : id) (name : string)
     (nm : names_map) : names_map =
@@ -297,12 +301,12 @@ let names_map_add_assumed_function (id_to_string : id -> string)
     
     Also note that at some point, we thought about trying to reuse names of
     variables which are not used anymore, like here:
-    ```
-    let x = ... in
-    ...
-    let x0 = ... in // We could use the name "x" if `x` is not used below
-    ...
-    ```
+    {[
+      let x = ... in
+      ...
+      let x0 = ... in // We could use the name "x" if [x] is not used below
+      ...
+    ]}
     
     However it is a good idea to keep things as they are for F*: as F* is
     designed for extrinsic proofs, a proof about a function follows this
@@ -322,13 +326,6 @@ let basename_to_unique (names_set : StringSet.t)
   in
   if StringSet.mem basename names_set then gen 0 else basename
 
-type extraction_ctx = {
-  trans_ctx : trans_ctx;
-  names_map : names_map;
-  fmt : formatter;
-  indent_incr : int;
-      (** The indent increment we insert whenever we need to indent more *)
-}
 (** Extraction context.
 
     Note that the extraction context contains information coming from the
@@ -336,6 +333,13 @@ type extraction_ctx = {
     we use the region information to generate the names of the backward
     functions, etc.
  *)
+type extraction_ctx = {
+  trans_ctx : trans_ctx;
+  names_map : names_map;
+  fmt : formatter;
+  indent_incr : int;
+      (** The indent increment we insert whenever we need to indent more *)
+}
 
 (** Debugging function *)
 let id_to_string (id : id) (ctx : extraction_ctx) : string =
@@ -495,7 +499,7 @@ let ctx_add_type_var (basename : string) (id : TypeVarId.id)
   let ctx = ctx_add (TypeVarId id) name ctx in
   (ctx, name)
 
-(** See [ctx_add_type_var] *)
+(** See {!ctx_add_type_var} *)
 let ctx_add_type_vars (vars : (string * TypeVarId.id) list)
     (ctx : extraction_ctx) : extraction_ctx * string list =
   List.fold_left_map
@@ -511,7 +515,7 @@ let ctx_add_var (basename : string) (id : VarId.id) (ctx : extraction_ctx) :
   let ctx = ctx_add (VarId id) name ctx in
   (ctx, name)
 
-(** See [ctx_add_var] *)
+(** See {!ctx_add_var} *)
 let ctx_add_vars (vars : var list) (ctx : extraction_ctx) :
     extraction_ctx * string list =
   List.fold_left_map
@@ -685,9 +689,9 @@ let compute_type_decl_name (fmt : formatter) (def : type_decl) : string =
 let default_fun_suffix (num_region_groups : int) (rg : region_group_info option)
     ((keep_fwd, num_backs) : bool * int) : string =
   (* There are several cases:
-     - [rg] is `Some`: this is a forward function:
+     - [rg] is [Some]: this is a forward function:
        - we add "_fwd"
-     - [rg] is `None`: this is a backward function:
+     - [rg] is [None]: this is a backward function:
        - this function has one extracted backward function:
          - if the forward function has been filtered, we add "_fwd_back":
            the forward function is useless, so the unique backward function
diff --git a/src/PureTypeCheck.ml b/src/PureTypeCheck.ml
index 5aefb0be..caad8a58 100644
--- a/src/PureTypeCheck.ml
+++ b/src/PureTypeCheck.ml
@@ -20,7 +20,7 @@ let get_adt_field_types (type_decls : type_decl TypeDeclId.Map.t)
       (* Assumed type *)
       match aty with
       | State ->
-          (* `State` is opaque *)
+          (* [State] is opaque *)
           raise (Failure "Unreachable: `State` values are opaque")
       | Result ->
           let ty = Collections.List.to_cons_nil tys in
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index c3d4c983..39f3d76a 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -3,9 +3,9 @@ open Pure
 (** Default logger *)
 let log = Logging.pure_utils_log
 
+(** We use this type as a key for lookups *)
 type regular_fun_id = A.fun_id * T.RegionGroupId.id option
 [@@deriving show, ord]
-(** We use this type as a key for lookups *)
 
 module RegularFunIdOrderedType = struct
   type t = regular_fun_id
@@ -72,7 +72,7 @@ let make_type_subst (vars : type_var list) (tys : ty list) : TypeVarId.id -> ty
   in
   fun id -> TypeVarId.Map.find id mp
 
-(** Retrieve the list of fields for the given variant of a [type_decl].
+(** Retrieve the list of fields for the given variant of a {!Pure.type_decl}.
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
@@ -157,7 +157,7 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool =
 
 (** We use this to check whether we need to add parentheses around expressions.
     We only look for outer monadic let-bindings.
-    This is used when printing the branches of `if ... then ... else ...`.
+    This is used when printing the branches of [if ... then ... else ...].
  *)
 let rec let_group_requires_parentheses (e : texpression) : bool =
   match e.e with
@@ -179,7 +179,7 @@ let is_global (e : texpression) : bool =
 let is_const (e : texpression) : bool =
   match e.e with Const _ -> true | _ -> false
 
-(** Remove the external occurrences of [Meta] *)
+(** Remove the external occurrences of {!Meta} *)
 let rec unmeta (e : texpression) : texpression =
   match e.e with Meta (_, e) -> unmeta e | _ -> e
 
@@ -202,9 +202,9 @@ let mk_arrows (inputs : ty list) (output : ty) =
   in
   aux inputs
 
-(** Destruct an `App` expression into an expression and a list of arguments.
+(** Destruct an [App] expression into an expression and a list of arguments.
 
-    We simply destruct the expression as long as it is of the form `App (f, x)`.
+    We simply destruct the expression as long as it is of the form [App (f, x)].
  *)
 let destruct_apps (e : texpression) : texpression * texpression list =
   let rec aux (args : texpression list) (e : texpression) :
@@ -213,7 +213,7 @@ let destruct_apps (e : texpression) : texpression * texpression list =
   in
   aux [] e
 
-(** Make an `App (app, arg)` expression *)
+(** Make an [App (app, arg)] expression *)
 let mk_app (app : texpression) (arg : texpression) : texpression =
   match app.ty with
   | Arrow (ty0, ty1) ->
@@ -224,7 +224,7 @@ let mk_app (app : texpression) (arg : texpression) : texpression =
       { e; ty }
   | _ -> raise (Failure "Expected an arrow type")
 
-(** The reverse of [destruct_app] *)
+(** The reverse of {!destruct_apps} *)
 let mk_apps (app : texpression) (args : texpression list) : texpression =
   List.fold_left (fun app arg -> mk_app app arg) app args
 
@@ -374,7 +374,7 @@ let mk_simpl_tuple_pattern (vl : typed_pattern list) : typed_pattern =
       let value = PatAdt { variant_id = None; field_values = vl } in
       { value; ty }
 
-(** Similar to [mk_simpl_tuple_pattern] *)
+(** Similar to {!mk_simpl_tuple_pattern} *)
 let mk_simpl_tuple_texpression (vl : texpression list) : texpression =
   match vl with
   | [ v ] -> v
diff --git a/src/StringUtils.ml b/src/StringUtils.ml
index 601249ca..0fd46136 100644
--- a/src/StringUtils.ml
+++ b/src/StringUtils.ml
@@ -32,7 +32,7 @@ let lowercase_ascii = Char.lowercase_ascii
 let uppercase_ascii = Char.uppercase_ascii
 
 (** Using buffers as per:
-    [https://stackoverflow.com/questions/29957418/how-to-convert-char-list-to-string-in-ocaml]
+    {{: https://stackoverflow.com/questions/29957418/how-to-convert-char-list-to-string-in-ocaml} stackoverflow}
  *)
 let string_of_chars (chars : char list) : string =
   let buf = Buffer.create (List.length chars) in
diff --git a/src/Substitute.ml b/src/Substitute.ml
index b99baafa..5e5858de 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -34,7 +34,7 @@ let rec ty_substitute (rsubst : 'r1 -> 'r2)
   | Str -> Str
   | TypeVar vid -> tsubst vid
 
-(** Convert an [rty] to an [ety] by erasing the region variables *)
+(** Convert an {!T.rty} to an {!T.ety} by erasing the region variables *)
 let erase_regions (ty : T.rty) : T.ety =
   ty_substitute (fun _ -> T.Erased) (fun vid -> T.TypeVar vid) ty
 
@@ -43,7 +43,7 @@ let erase_regions (ty : T.rty) : T.ety =
     Return the list of new regions and appropriate substitutions from the
     original region variables to the fresh regions.
     
-    TODO: simplify? we only need the subst `T.RegionVarId.id -> T.RegionId.id`
+    TODO: simplify? we only need the subst [T.RegionVarId.id -> T.RegionId.id]
   *)
 let fresh_regions_with_substs (region_vars : T.region_var list) :
     T.RegionId.id list
diff --git a/src/SymbolicAst.ml b/src/SymbolicAst.ml
index ec2a80ca..604a7948 100644
--- a/src/SymbolicAst.ml
+++ b/src/SymbolicAst.ml
@@ -8,15 +8,6 @@ module V = Values
 module E = Expressions
 module A = LlbcAst
 
-type mplace = {
-  bv : Contexts.binder;
-      (** It is important that we store the binder, and not just the variable id,
-          because the most important information in a place is the name of the
-          variable!
-       *)
-  projection : E.projection;
-      (** We store the projection because we can, but it is actually not that useful *)
-}
 (** "Meta"-place: a place stored as meta-data.
 
     Whenever we need to introduce new symbolic variables, for instance because
@@ -26,6 +17,15 @@ type mplace = {
     We later use this place information to generate meaningful name, to prettify
     the generated code.
  *)
+type mplace = {
+  bv : Contexts.binder;
+      (** It is important that we store the binder, and not just the variable id,
+          because the most important information in a place is the name of the
+          variable!
+       *)
+  projection : E.projection;
+      (** We store the projection because we can, but it is actually not that useful *)
+}
 
 type call_id =
   | Fun of A.fun_id * V.FunCallId.id
@@ -52,7 +52,7 @@ type meta =
   | Assignment of mplace * V.typed_value * mplace option
       (** We generated an assignment (destination, assigned value, src) *)
 
-(** **Rk.:** here, [expression] is not at all equivalent to the expressions
+(** **Rk.:** here, {!expression} is not at all equivalent to the expressions
     used in LLBC: they are a first step towards lambda-calculus expressions.
  *)
 type expression =
@@ -60,7 +60,7 @@ type expression =
       (** There are two cases:
           - the AST is for a forward function: the typed value should contain
             the value which was in the return variable
-          - the AST is for a backward function: the typed value should be `None`
+          - the AST is for a backward function: the typed value should be [None]
        *)
   | Panic
   | FunCall of call * expression
@@ -91,7 +91,7 @@ and expansion =
       (T.VariantId.id option * V.symbolic_value list * expression) list
       (** ADT expansion *)
   | ExpandBool of expression * expression
-      (** A boolean expansion (i.e, an `if ... then ... else ...`) *)
+      (** A boolean expansion (i.e, an [if ... then ... else ...]) *)
   | ExpandInt of
       T.integer_type * (V.scalar_value * expression) list * expression
       (** An integer expansion (i.e, a switch over an integer). The last
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 77c5e0e8..de4fb4c1 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -14,7 +14,7 @@ let log = L.symbolic_to_pure_log
 
 type config = {
   filter_useless_back_calls : bool;
-      (** If `true`, filter the useless calls to backward functions.
+      (** If [true], filter the useless calls to backward functions.
        
           The useless calls are calls to backward functions which have no outputs.
           This case happens if the original Rust function only takes *shared* borrows
@@ -73,6 +73,10 @@ type fun_context = {
 
 type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
 
+(** Whenever we translate a function call or an ended abstraction, we
+    store the related information (this is useful when translating ended
+    children abstractions).
+ *)
 type call_info = {
   forward : S.call;
   forward_inputs : texpression list;
@@ -88,11 +92,8 @@ type call_info = {
           TODO: remove? it is also in the bs_ctx ("abstractions" field)
        *)
 }
-(** Whenever we translate a function call or an ended abstraction, we
-    store the related information (this is useful when translating ended
-    children abstractions).
- *)
 
+(** Body synthesis context *)
 type bs_ctx = {
   type_context : type_context;
   fun_context : fun_context;
@@ -100,7 +101,7 @@ type bs_ctx = {
   fun_decl : A.fun_decl;
   bid : T.RegionGroupId.id option;  (** TODO: rename *)
   sg : fun_sig;
-      (** The function signature - useful in particular to translate `Panic` *)
+      (** The function signature - useful in particular to translate [Panic] *)
   sv_to_var : var V.SymbolicValueId.Map.t;
       (** Whenever we encounter a new symbolic value (introduced because of
           a symbolic expansion or upon ending an abstraction, for instance)
@@ -120,7 +121,6 @@ type bs_ctx = {
   abstractions : (V.abs * texpression list) V.AbstractionId.Map.t;
       (** The ended abstractions we encountered so far, with their additional input arguments  *)
 }
-(** Body synthesis context *)
 
 let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
   let env = VarId.Map.empty in
@@ -556,14 +556,14 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
     | None -> []
     | Some gid ->
         (* For now, we don't allow nested borrows, so the additional inputs to the
-         * backward function can only come from borrows that were returned like
-         * in (for the backward function we introduce for 'a):
-         * ```
-         * fn f<'a>(...) -> &'a mut u32;
-         * ```
-         * Upon ending the abstraction for 'a, we need to get back the borrow
-         * the function returned.
-         *)
+           backward function can only come from borrows that were returned like
+           in (for the backward function we introduce for 'a):
+           {[
+             fn f<'a>(...) -> &'a mut u32;
+           ]}
+           Upon ending the abstraction for 'a, we need to get back the borrow
+           the function returned.
+        *)
         List.filter_map (translate_back_ty_for_gid gid) [ sg.output ]
   in
   (* Does the function take a state as input, does it return a state and can
@@ -585,14 +585,14 @@ let translate_fun_sig (fun_infos : FA.fun_info A.FunDeclId.Map.t)
         ([ None ], [ translate_fwd_ty types_infos sg.output ])
     | Some gid ->
         (* This is a backward function: there might be several outputs.
-         * The outputs are the borrows inside the regions of the abstractions
-         * and which are present in the input values. For instance, see:
-         * ```
-         * fn f<'a>(x : &'a mut u32) -> ...;
-         * ```
-         * Upon ending the abstraction for 'a, we give back the borrow which
-         * was consumed through the `x` parameter.
-         *)
+           The outputs are the borrows inside the regions of the abstractions
+           and which are present in the input values. For instance, see:
+           {[
+             fn f<'a>(x : &'a mut u32) -> ...;
+           ]}
+           Upon ending the abstraction for 'a, we give back the borrow which
+           was consumed through the [x] parameter.
+        *)
         let outputs =
           List.map
             (fun (name, input_ty) ->
@@ -692,7 +692,7 @@ let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) :
 let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
   V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var
 
-(** Peel boxes as long as the value is of the form `Box<T>` *)
+(** Peel boxes as long as the value is of the form [Box<T>] *)
 let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
   match (v.value, v.ty) with
   | V.Adt av, T.Adt (T.Assumed T.Box, _, _) -> (
@@ -795,14 +795,14 @@ let rec typed_value_to_texpression (ctx : bs_ctx) (v : V.typed_value) :
     Consumed values are rvalues, because when an abstraction ends, we
     introduce a call to a backward function in the synthesized program,
     which takes as inputs those consumed values:
-    ```
-    // Rust:
-    fn choose<'a>(b: bool, x : &'a mut u32, y : &'a mut u32) -> &'a mut u32;
-    
-    // Synthesis:
-    let ... = choose_back b x y nz in
-                                ^^
-    ```
+    {[
+      // Rust:
+      fn choose<'a>(b: bool, x : &'a mut u32, y : &'a mut u32) -> &'a mut u32;
+
+      // Synthesis:
+      let ... = choose_back b x y nz in
+                                  ^^
+    ]}
  *)
 let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
     texpression option =
@@ -931,10 +931,10 @@ let translate_opt_mplace (p : S.mplace option) : mplace option =
     Given back values are patterns, because when an abstraction ends, we
     introduce a call to a backward function in the synthesized program,
     which introduces new values:
-    ```
-    let (nx, ny) = f_back ... in
-        ^^^^^^^^
-    ```
+    {[
+      let (nx, ny) = f_back ... in
+          ^^^^^^^^
+    ]}
     
     [mp]: it is possible to provide some meta-place information, to guide
     the heuristics which later find pretty names for the variables.
@@ -957,7 +957,7 @@ let rec typed_avalue_to_given_back (mp : mplace option) (av : V.typed_avalue)
         in
         let field_values = List.filter_map (fun x -> x) field_values in
         (* For now, only tuples can contain borrows - note that if we gave
-         * something like a `&mut Vec` to a function, we give give back the
+         * something like a [&mut Vec] to a function, we give give back the
          * vector value upon visiting the "abstraction borrow" node *)
         let adt_id, _, _ = TypesUtils.ty_as_adt av.ty in
         match adt_id with
@@ -1089,7 +1089,7 @@ and translate_panic (ctx : bs_ctx) : texpression =
   (* Note that only forward functions return a state *)
   let output_ty = mk_simpl_tuple_ty ctx.sg.doutputs in
   if ctx.sg.info.effect_info.output_state then
-    (* Create the `Fail` value *)
+    (* Create the [Fail] value *)
     let ret_ty = mk_simpl_tuple_ty [ mk_state_ty; output_ty ] in
     let ret_v = mk_result_fail_texpression ret_ty in
     ret_v
@@ -1099,8 +1099,8 @@ and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression
     =
   (* There are two cases:
      - either we are translating a forward function, in which case the optional
-       value should be `Some` (it is the returned value)
-     - or we are translating a backward function, in which case it should be `None`
+       value should be [Some] (it is the returned value)
+     - or we are translating a backward function, in which case it should be [None]
   *)
   match ctx.bid with
   | None ->
@@ -1136,7 +1136,7 @@ and translate_return (opt_v : V.typed_value option) (ctx : bs_ctx) : texpression
       in
       let field_values = List.map mk_texpression_from_var backward_outputs in
       (* Backward functions never return a state *)
-      (* TODO: we should use a `fail` function, it would be cleaner *)
+      (* TODO: we should use a [fail] function, it would be cleaner *)
       let ret_value = mk_simpl_tuple_texpression field_values in
       let ret_value = mk_result_return_texpression ret_value in
       ret_value
@@ -1262,18 +1262,18 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       assert (abs.back_id = bid);
 
       (* The translation is done as follows:
-       * - for a given backward function, we choose a set of variables `v_i`
+       * - for a given backward function, we choose a set of variables [v_i]
        * - when we detect the ended input abstraction which corresponds
-       *   to the backward function, and which consumed the values `consumed_i`,
+       *   to the backward function, and which consumed the values [consumed_i],
        *   we introduce:
-       *   ```
-       *   let v_i = consumed_i in
-       *   ...
-       *   ```
-       *   Then, when we reach the `Return` node, we introduce:
-       *   ```
-       *   (v_i)
-       *   ```
+       *   {[
+         *   let v_i = consumed_i in
+         *   ...
+       *   ]}
+       *   Then, when we reach the [Return] node, we introduce:
+       *   {[
+         *   (v_i)
+       *   ]}
        * *)
       (* First, get the given back variables *)
       let given_back_variables =
@@ -1321,7 +1321,7 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       (* Retrieve the values given back by this function: those are the output
        * values. We rely on the fact that there are no nested borrows to use the
        * meta-place information from the input values given to the forward function
-       * (we need to add `None` for the return avalue) *)
+       * (we need to add [None] for the return avalue) *)
       let output_mpl =
         List.append (List.map translate_opt_mplace call.args_places) [ None ]
       in
@@ -1402,34 +1402,33 @@ and translate_end_abstraction (config : config) (abs : V.abs) (e : S.expression)
       else mk_let effect_info.can_fail output call next_e
   | V.SynthRet ->
       (* If we end the abstraction which consumed the return value of the function
-       * we are synthesizing, we get back the borrows which were inside. Those borrows
-       * are actually input arguments of the backward function we are synthesizing.
-       * So we simply need to introduce proper let bindings.
-       * 
-       * For instance:
-       * ```
-       * fn id<'a>(x : &'a mut u32) -> &'a mut u32 {
-       *   x
-       * }
-       * ```
-       *
-       * Upon ending the return abstraction for 'a, we get back the borrow for `x`.
-       * This new value is the second argument of the backward function:
-       * ```
-       * let id_back x nx = nx
-       * ```
-       *
-       * In practice, upon ending this abstraction we introduce a useless
-       * let-binding:
-       * ```
-       * let id_back x nx =
-       *   let s = nx in // the name `s` is not important (only collision matters)
-       *   ...
-       * ```
-       *
-       * This let-binding later gets inlined, during a micro-pass.
-       * 
-       * *)
+         we are synthesizing, we get back the borrows which were inside. Those borrows
+         are actually input arguments of the backward function we are synthesizing.
+         So we simply need to introduce proper let bindings.
+
+         For instance:
+         {[
+           fn id<'a>(x : &'a mut u32) -> &'a mut u32 {
+             x
+           }
+         ]}
+
+         Upon ending the return abstraction for 'a, we get back the borrow for [x].
+         This new value is the second argument of the backward function:
+         {[
+           let id_back x nx = nx
+         ]}
+
+         In practice, upon ending this abstraction we introduce a useless
+         let-binding:
+         {[
+           let id_back x nx =
+             let s = nx in // the name [s] is not important (only collision matters)
+             ...
+         ]}
+
+         This let-binding later gets inlined, during a micro-pass.
+      *)
       (* First, retrieve the list of variables used for the inputs for the
        * backward function *)
       let inputs = T.RegionGroupId.Map.find abs.back_id ctx.backward_inputs in
@@ -1573,7 +1572,7 @@ and translate_expansion (config : config) (p : S.mplace option)
                 | _ -> raise (Failure "Unreachable")
               in
               (* We simply introduce an assignment - the box type is the
-               * identity when extracted (`box a == a`) *)
+               * identity when extracted ([box a == a]) *)
               let monadic = false in
               mk_let monadic
                 (mk_typed_pattern_from_var var None)
diff --git a/src/Translate.ml b/src/Translate.ml
index 8024d910..8f3b94c4 100644
--- a/src/Translate.ml
+++ b/src/Translate.ml
@@ -25,15 +25,15 @@ type config = {
        *)
   test_unit_functions : bool;
       (** If true, insert tests in the generated files to check that the
-          unit functions normalize to `Success _`.
+          unit functions normalize to [Success _].
           
           For instance, in F* it generates code like this:
-          ```
-          let _ = assert_norm (FUNCTION () = Success ())
-          ```
+          {[
+            let _ = assert_norm (FUNCTION () = Success ())
+          ]}
        *)
   extract_decreases_clauses : bool;
-      (** If `true`, insert `decreases` clauses for all the recursive definitions.
+      (** If [true], insert [decreases] clauses for all the recursive definitions.
 
           The body of such clauses must be defined by the user.
        *)
@@ -44,11 +44,11 @@ type config = {
        *)
 }
 
-type symbolic_fun_translation = V.symbolic_value list * SA.expression
 (** The result of running the symbolic interpreter on a function:
     - the list of symbolic values used for the input values
     - the generated symbolic AST
 *)
+type symbolic_fun_translation = V.symbolic_value list * SA.expression
 
 (** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
     for the forward function and the backward functions.
@@ -355,6 +355,7 @@ let translate_module_to_pure (config : C.partial_config)
   (* Return *)
   (trans_ctx, type_decls, pure_translations)
 
+(** Extraction context *)
 type gen_ctx = {
   crate : Crates.llbc_crate;
   extract_ctx : PureToExtract.extraction_ctx;
@@ -362,7 +363,6 @@ type gen_ctx = {
   trans_funs : (bool * pure_fun_translation) A.FunDeclId.Map.t;
   functions_with_decreases_clause : A.FunDeclId.Set.t;
 }
-(** Extraction context *)
 
 type gen_config = {
   mp_config : Micro.config;
@@ -372,14 +372,14 @@ type gen_config = {
   extract_template_decreases_clauses : bool;
   extract_fun_decls : bool;
   extract_transparent : bool;
-      (** If `true`, extract the transparent declarations, otherwise ignore. *)
+      (** If [true], extract the transparent declarations, otherwise ignore. *)
   extract_opaque : bool;
-      (** If `true`, extract the opaque declarations, otherwise ignore. *)
+      (** If [true], extract the opaque declarations, otherwise ignore. *)
   extract_state_type : bool;
-      (** If `true`, generate a definition/declaration for the state type *)
+      (** If [true], generate a definition/declaration for the state type *)
   interface : bool;
-      (** `true` if we generate an interface file, `false` otherwise.
-          For now, this only impacts whether we use `val` or `assume val` for the
+      (** [true] if we generate an interface file, [false] otherwise.
+          For now, this only impacts whether we use [val] or [assume val] for the
           opaque definitions. In the future, we might want to extract all the
           declarations in an interface file, together with an implementation file
           if needed.
@@ -586,7 +586,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
 
   (* Print the headers.
    * Note that we don't use the OCaml formatter for purpose: we want to control
-   * line insertion (we have to make sure that some instructions like `open MODULE`
+   * line insertion (we have to make sure that some instructions like [open MODULE]
    * are printed on one line!).
    * This is ok as long as we end up with a line break, so that the formatter's
    * internal count is consistent with the state of the file.
diff --git a/src/Types.ml b/src/Types.ml
index 48dd9ab0..326ef76f 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -84,10 +84,10 @@ let all_int_types = List.append all_signed_int_types all_unsigned_int_types
 type ref_kind = Mut | Shared [@@deriving show, ord]
 type assumed_ty = Box | Vec | Option [@@deriving show, ord]
 
-(** The variant id for `Option::None` *)
+(** The variant id for [Option::None] *)
 let option_none_id = VariantId.of_int 0
 
-(** The variant id for `Option::Some` *)
+(** The variant id for [Option::Some] *)
 let option_some_id = VariantId.of_int 1
 
 (** Type identifier for ADTs.
@@ -125,7 +125,7 @@ class ['self] map_ty_base =
 
 type 'r ty =
   | Adt of type_id * 'r list * 'r ty list
-      (** [Adt] encodes ADTs, tuples and assumed types *)
+      (** {!Adt} encodes ADTs, tuples and assumed types *)
   | TypeVar of TypeVarId.id
   | Bool
   | Char
@@ -143,7 +143,7 @@ type 'r ty =
         name = "iter_ty";
         variety = "iter";
         ancestors = [ "iter_ty_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
       },
@@ -152,7 +152,7 @@ type 'r ty =
         name = "map_ty";
         variety = "map";
         ancestors = [ "map_ty_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
         polymorphic = false;
       }]
diff --git a/src/TypesAnalysis.ml b/src/TypesAnalysis.ml
index 0d23e92b..60ce5149 100644
--- a/src/TypesAnalysis.ml
+++ b/src/TypesAnalysis.ml
@@ -7,8 +7,8 @@ type subtype_info = {
 }
 [@@deriving show]
 
+(** See {!type_decl_info} *)
 type type_param_info = subtype_info [@@deriving show]
-(** See [type_decl_info] *)
 
 type expl_info = subtype_info [@@deriving show]
 
@@ -23,26 +23,26 @@ type type_borrows_info = {
 }
 [@@deriving show]
 
+(** Generic definition *)
 type 'p g_type_info = {
   borrows_info : type_borrows_info;
       (** Various informations about the borrows *)
   param_infos : 'p;  (** Gives information about the type parameters *)
 }
 [@@deriving show]
-(** Generic definition *)
 
-type type_decl_info = type_param_info list g_type_info [@@deriving show]
 (** Information about a type definition. *)
+type type_decl_info = type_param_info list g_type_info [@@deriving show]
 
-type ty_info = type_borrows_info [@@deriving show]
 (** Information about a type. *)
+type ty_info = type_borrows_info [@@deriving show]
 
-type partial_type_info = type_param_info list option g_type_info
-[@@deriving show]
 (** Helper definition.
 
-    Allows us to factorize code: [analyze_full_ty] is used both to analyze
+    Allows us to factorize code: {!analyze_full_ty} is used both to analyze
     type definitions and types. *)
+type partial_type_info = type_param_info list option g_type_info
+[@@deriving show]
 
 type type_infos = type_decl_info TypeDeclId.Map.t [@@deriving show]
 
@@ -129,11 +129,11 @@ let analyze_full_ty (r_is_static : 'r -> bool) (updated : bool ref)
         | None -> ty_info
         | Some param_infos ->
             let param_info = TypeVarId.nth param_infos var_id in
-            (* Set `under_borrow` *)
+            (* Set [under_borrow] *)
             let under_borrow =
               check_update_bool param_info.under_borrow expl_info.under_borrow
             in
-            (* Set `under_nested_borrows` *)
+            (* Set [under_nested_borrows] *)
             let under_mut_borrow =
               check_update_bool param_info.under_mut_borrow
                 expl_info.under_mut_borrow
@@ -318,7 +318,7 @@ let analyze_type_declarations (type_decls : type_decl TypeDeclId.Map.t)
     we have already analyzed the type definitions in the context.
  *)
 let analyze_ty (infos : type_infos) (ty : 'r ty) : ty_info =
-  (* We don't use `updated` but need to give it as parameter *)
+  (* We don't use [updated] but need to give it as parameter *)
   let updated = ref false in
   (* We don't need to compute whether the type contains 'static or not *)
   let r_is_static _ = false in
diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml
index b5ea6fca..7531dd8b 100644
--- a/src/TypesUtils.ml
+++ b/src/TypesUtils.ml
@@ -5,7 +5,7 @@ module TA = TypesAnalysis
 let type_decl_is_opaque (d : type_decl) : bool =
   match d.kind with Struct _ | Enum _ -> false | Opaque -> true
 
-(** Retrieve the list of fields for the given variant of a [type_decl].
+(** Retrieve the list of fields for the given variant of a {!Types.type_decl}.
 
     Raises [Invalid_argument] if the arguments are incorrect.
  *)
@@ -25,7 +25,7 @@ let type_decl_get_fields (def : type_decl)
              - def: " ^ show_type_decl def ^ "\n- opt_variant_id: "
           ^ opt_variant_id))
 
-(** Return [true] if a [ty] is actually `unit` *)
+(** Return [true] if a {!Types.ty} is actually [unit] *)
 let ty_is_unit (ty : 'r ty) : bool =
   match ty with Adt (Tuple, [], []) -> true | _ -> false
 
@@ -51,13 +51,13 @@ let mk_unit_ty : 'r ty = Adt (Tuple, [], [])
 (** The usize type *)
 let mk_usize_ty : 'r ty = Integer Usize
 
-(** Deconstruct a type of the form `Box<T>` to retrieve the `T` inside *)
+(** Deconstruct a type of the form [Box<T>] to retrieve the [T] inside *)
 let ty_get_box (box_ty : ety) : ety =
   match box_ty with
   | Adt (Assumed Box, [], [ boxed_ty ]) -> boxed_ty
   | _ -> failwith "Not a boxed type"
 
-(** Deconstruct a type of the form `&T` or `&mut T` to retrieve the `T` (and
+(** Deconstruct a type of the form [&T] or [&mut T] to retrieve the [T] (and
     the borrow kind, etc.)
  *)
 let ty_get_ref (ty : 'r ty) : 'r * 'r ty * ref_kind =
@@ -99,7 +99,8 @@ let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool =
   let ty_regions = rty_regions ty in
   not (RegionId.Set.disjoint ty_regions regions)
 
-(** Convert an [ety], containing no region variables, to an [rty] or an [sty].
+(** Convert an {!Types.ety}, containing no region variables, to an {!Types.rty}
+    or an {!Types.sty}.
 
     In practice, it is the identity.
  *)
@@ -127,7 +128,7 @@ let ety_no_regions_to_sty (ty : ety) : sty = ety_no_regions_to_gr_ty ty
 (** Retuns true if the type contains borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with `[]` when using `ety`,
+    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_borrows (infos : TA.type_infos) (ty : 'r ty) : bool =
@@ -137,7 +138,7 @@ let ty_has_borrows (infos : TA.type_infos) (ty : 'r ty) : bool =
 (** Retuns true if the type contains nested borrows.
 
     Note that we can't simply explore the type and look for regions: sometimes
-    we erase the lists of regions (by replacing them with `[]` when using `ety`,
+    we erase the lists of regions (by replacing them with [[]] when using {!Types.ety},
     and when a type uses 'static this region doesn't appear in the region parameters.
  *)
 let ty_has_nested_borrows (infos : TA.type_infos) (ty : 'r ty) : bool =
@@ -149,7 +150,7 @@ let ty_has_borrow_under_mut (infos : TA.type_infos) (ty : 'r ty) : bool =
   let info = TA.analyze_ty infos ty in
   info.TA.contains_borrow_under_mut
 
-(** Check if a [ty] contains regions from a given set *)
+(** Check if a {!Types.ty} contains regions from a given set *)
 let ty_has_regions_in_set (rset : RegionId.Set.t) (ty : rty) : bool =
   let obj =
     object
diff --git a/src/Values.ml b/src/Values.ml
index fb927fb5..e404f40d 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -28,12 +28,12 @@ let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
 
 let show_big_int (bi : big_int) : string = Z.to_string bi
 
-type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
 (** A scalar value
 
     Note that we use unbounded integers everywhere.
     We then harcode the boundaries for the different types.
  *)
+type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
 
 (** A constant value *)
 type constant_value =
@@ -68,15 +68,15 @@ type sv_kind =
   | Global  (** The value is a global *)
 [@@deriving show]
 
+(** A symbolic value *)
 type symbolic_value = {
   sv_kind : sv_kind;
   sv_id : SymbolicValueId.id;
   sv_ty : rty;
 }
 [@@deriving show]
-(** A symbolic value *)
 
-(** Ancestor for [typed_value] iter visitor *)
+(** Ancestor for {!typed_value} iter visitor *)
 class ['self] iter_typed_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.iter
@@ -86,7 +86,7 @@ class ['self] iter_typed_value_base =
     method visit_ety : 'env -> ety -> unit = fun _ _ -> ()
   end
 
-(** Ancestor for [typed_value] map visitor for *)
+(** Ancestor for {!typed_value} map visitor for *)
 class ['self] map_typed_value_base =
   object (_self : 'self)
     inherit [_] VisitorsRuntime.map
@@ -140,7 +140,7 @@ and borrow_content =
   | InactivatedMutBorrow of mvalue * (BorrowId.id[@opaque])
       (** An inactivated mut borrow.
 
-          This is used to model [two-phase borrows](https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html).
+          This is used to model {{: https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html} two-phase borrows}.
           When evaluating a two-phase mutable borrow, we first introduce an inactivated
           borrow which behaves like a shared borrow, until the moment we actually *use*
           the borrow: at this point, we end all the other shared borrows (or inactivated
@@ -149,19 +149,19 @@ and borrow_content =
           mutable borrow.
           
           A simple use case of two-phase borrows:
-          ```
-          let mut v = Vec::new();
-          v.push(v.len());
-          ```
+          {[
+            let mut v = Vec::new();
+            v.push(v.len());
+          ]}
           
           This gets desugared to (something similar to) the following MIR:
-          ```
-          v = Vec::new();
-          v1 = &mut v;
-          v2 = &v; // We need this borrow, but v has already been mutably borrowed!
-          l = Vec::len(move v2);
-          Vec::push(move v1, move l); // In practice, v1 gets activated only here
-          ```
+          {[
+            v = Vec::new();
+            v1 = &mut v;
+            v2 = &v; // We need this borrow, but v has already been mutably borrowed!
+            l = Vec::len(move v2);
+            Vec::push(move v1, move l); // In practice, v1 gets activated only here
+          ]}
           
           The meta-value is used for the same purposes as with shared borrows,
           at the exception that in case of inactivated borrows it is not
@@ -185,7 +185,6 @@ and loan_content =
           borrows, and extremely useful when giving shared values to abstractions).
        *)
 
-and mvalue = typed_value
 (** "Meta"-value: information we store for the synthesis.
 
      Note that we never automatically visit the meta-values with the
@@ -195,7 +194,9 @@ and mvalue = typed_value
      TODO: we may want to create wrappers, to prevent accidently mixing meta
      values and regular values.
  *)
+and mvalue = typed_value
 
+(** "Regular" typed value (we map variables to typed values) *)
 and typed_value = { value : value; ty : ety }
 [@@deriving
   show,
@@ -204,7 +205,7 @@ and typed_value = { value : value; ty : ety }
         name = "iter_typed_value_visit_mvalue";
         variety = "iter";
         ancestors = [ "iter_typed_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -212,33 +213,34 @@ and typed_value = { value : value; ty : ety }
         name = "map_typed_value_visit_mvalue";
         variety = "map";
         ancestors = [ "map_typed_value_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
-(** "Regular" typed value (we map variables to typed values) *)
 
-(** We have to override the [visit_mvalue] method, to ignore meta-values *)
+(** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
+    to ignore meta-values *)
 class ['self] iter_typed_value =
   object (_self : 'self)
     inherit [_] iter_typed_value_visit_mvalue
     method! visit_mvalue : 'env -> mvalue -> unit = fun _ _ -> ()
   end
 
-(** We have to override the [visit_mvalue] method, to ignore meta-values *)
+(** We have to override the {!iter_typed_value_visit_mvalue.visit_mvalue} method,
+    to ignore meta-values *)
 class ['self] map_typed_value =
   object (_self : 'self)
     inherit [_] map_typed_value_visit_mvalue
     method! visit_mvalue : 'env -> mvalue -> mvalue = fun _ x -> x
   end
 
-type msymbolic_value = symbolic_value [@@deriving show]
 (** "Meta"-symbolic value.
 
-     See the explanations for [mvalue]
+     See the explanations for {!mvalue}
 
      TODO: we may want to create wrappers, to prevent mixing meta values
      and regular values.
  *)
+type msymbolic_value = symbolic_value [@@deriving show]
 
 (** When giving shared borrows to functions (i.e., inserting shared borrows inside
     abstractions) we need to reborrow the shared values. When doing so, we lookup
@@ -259,10 +261,10 @@ type abstract_shared_borrow =
   | AsbProjReborrows of (symbolic_value[@opaque]) * (rty[@opaque])
 [@@deriving show]
 
-type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show]
 (** A set of abstract shared borrows *)
+type abstract_shared_borrows = abstract_shared_borrow list [@@deriving show]
 
-(** Ancestor for [aproj] iter visitor *)
+(** Ancestor for {!aproj} iter visitor *)
 class ['self] iter_aproj_base =
   object (_self : 'self)
     inherit [_] iter_typed_value
@@ -272,7 +274,7 @@ class ['self] iter_aproj_base =
       fun _ _ -> ()
   end
 
-(** Ancestor for [aproj] map visitor *)
+(** Ancestor for {!aproj} map visitor *)
 class ['self] map_aproj_base =
   object (_self : 'self)
     inherit [_] map_typed_value
@@ -291,21 +293,21 @@ type aproj =
           receive *several* (symbolic) given back values.
           
           This is the case in the following example:
-          ```
-          fn f<'a> (...) -> (&'a mut u32, &'a mut u32);
-          fn g<'b, 'c>(p : (&'b mut u32, &'c mut u32));
-          
-          let p = f(...);
-          g(move p);
-          
-          // Symbolic context after the call to g:
-          // abs'a {'a} { [s@0 <: (&'a mut u32, &'a mut u32)] }
-          //
-          // abs'b {'b} { (s@0 <: (&'b mut u32, &'c mut u32)) }
-          // abs'c {'c} { (s@0 <: (&'b mut u32, &'c mut u32)) }
-          ```
+          {[
+            fn f<'a> (...) -> (&'a mut u32, &'a mut u32);
+            fn g<'b, 'c>(p : (&'b mut u32, &'c mut u32));
+
+            let p = f(...);
+            g(move p);
+
+            // Symbolic context after the call to g:
+            // abs'a {'a} { [s@0 <: (&'a mut u32, &'a mut u32)] }
+            //
+            // abs'b {'b} { (s@0 <: (&'b mut u32, &'c mut u32)) }
+            // abs'c {'c} { (s@0 <: (&'b mut u32, &'c mut u32)) }
+          ]}
           
-          Upon evaluating the call to `f`, we introduce a symbolic value `s@0`
+          Upon evaluating the call to [f], we introduce a symbolic value [s@0]
           and a projector of loans (projector loans from the region 'c).
           This projector will later receive two given back values: one for
           'a and one for 'b.
@@ -313,13 +315,13 @@ type aproj =
           We accumulate those values in the list of projections (note that
           the meta value stores the value which was given back).
           
-          We can later end the projector of loans if `s@0` is not referenced
+          We can later end the projector of loans if [s@0] is not referenced
           anywhere in the context below a projector of borrows which intersects
           this projector of loans.
        *)
   | AProjBorrows of symbolic_value * rty
       (** Note that an AProjBorrows only operates on a value which is not below
-          a shared loan: under a shared loan, we use [abstract_shared_borrow].
+          a shared loan: under a shared loan, we use {!abstract_shared_borrow}.
           
           Also note that once given to a borrow projection, a symbolic value
           can't get updated/expanded: this means that we don't need to save
@@ -328,12 +330,12 @@ type aproj =
   | AEndedProjLoans of msymbolic_value * (msymbolic_value * aproj) list
       (** An ended projector of loans over a symbolic value.
       
-          See the explanations for [AProjLoans]
+          See the explanations for {!AProjLoans}
           
           Note that we keep the original symbolic value as a meta-value.
        *)
   | AEndedProjBorrows of msymbolic_value
-      (** The only purpose of [AEndedProjBorrows] is to store, for synthesis
+      (** The only purpose of {!AEndedProjBorrows} is to store, for synthesis
           purposes, the symbolic value which was generated and given back upon
           ending the borrow.
        *)
@@ -345,7 +347,7 @@ type aproj =
         name = "iter_aproj";
         variety = "iter";
         ancestors = [ "iter_aproj_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -353,13 +355,13 @@ type aproj =
         name = "map_aproj";
         variety = "map";
         ancestors = [ "map_aproj_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
 
 type region = RegionVarId.id Types.region [@@deriving show]
 
-(** Ancestor for [typed_avalue] iter visitor *)
+(** Ancestor for {!typed_avalue} iter visitor *)
 class ['self] iter_typed_avalue_base =
   object (_self : 'self)
     inherit [_] iter_aproj
@@ -371,7 +373,7 @@ class ['self] iter_typed_avalue_base =
       fun _ _ -> ()
   end
 
-(** Ancestor for [typed_avalue] map visitor *)
+(** Ancestor for {!typed_avalue} map visitor *)
 class ['self] map_typed_avalue_base =
   object (_self : 'self)
     inherit [_] map_aproj
@@ -420,7 +422,7 @@ and adt_avalue = {
 (** A loan content as stored in an abstraction.
 
     Note that the children avalues are independent of the parent avalues.
-    For instance, the child avalue contained in an [AMutLoan] will likely
+    For instance, the child avalue contained in an {!AMutLoan} will likely
     contain other, independent loans.
     Keeping track of the hierarchy is not necessary to maintain the borrow graph
     (which is the primary role of the abstractions), but it is necessary
@@ -433,36 +435,36 @@ and aloan_content =
          
           Example:
           ========
-          ```
-          fn f<'a>(...) -> &'a mut &'a mut u32;
-          
-          let px = f(...);
-          ```
+          {[
+            fn f<'a>(...) -> &'a mut &'a mut u32;
+
+            let px = f(...);
+          ]}
           
           We get (after some symbolic exansion):
-          ```
-          abs0 {
-            a_mut_loan l0 (a_mut_loan l1)
-          }
-          px -> mut_borrow l0 (mut_borrow @s1)
-          ```
+          {[
+            abs0 {
+              a_mut_loan l0 (a_mut_loan l1)
+            }
+            px -> mut_borrow l0 (mut_borrow @s1)
+          ]}
        *)
   | ASharedLoan of (BorrowId.Set.t[@opaque]) * typed_value * typed_avalue
       (** A shared loan owned by an abstraction.
 
           Example:
           ========
-          ```
-          fn f<'a>(...) -> &'a u32;
-          
-          let px = f(...);
-          ```
+          {[
+            fn f<'a>(...) -> &'a u32;
+
+            let px = f(...);
+          ]}
           
           We get:
-          ```
-          abs0 { a_shared_loan {l0} @s0 ⊥ }
-          px -> shared_loan l0
-          ```
+          {[
+            abs0 { a_shared_loan {l0} @s0 ⊥ }
+            px -> shared_loan l0
+          ]}
      *)
   | AEndedMutLoan of {
       child : typed_avalue;
@@ -480,20 +482,20 @@ and aloan_content =
       
           Example:
           ========
-          ```
-          abs0 { a_mut_loan l0 ⊥ }
-          x -> mut_borrow l0 (U32 3)
-          ```
+          {[
+            abs0 { a_mut_loan l0 ⊥ }
+            x -> mut_borrow l0 (U32 3)
+          ]}
           
-          After ending `l0`:
+          After ending [l0]:
           
-          ```
-          abs0 { a_ended_mut_loan { given_back = U32 3; child = ⊥; }
-          x -> ⊥
-          ```
+          {[
+            abs0 { a_ended_mut_loan { given_back = U32 3; child = ⊥; }
+            x -> ⊥
+          ]}
        *)
   | AEndedSharedLoan of typed_value * typed_avalue
-      (** Similar to [AEndedMutLoan] but in this case there are no avalues to
+      (** Similar to {!AEndedMutLoan} but in this case there are no avalues to
           give back. We keep the shared value because it now behaves as a
           "regular" value (which contains borrows we might want to end...).
        *)
@@ -502,55 +504,55 @@ and aloan_content =
       
           We need to keep track of ignored mutable loans, because we may have
           to apply projections on the values given back to those loans (say
-          you have a borrow of type `&'a mut &'b mut`, in the abstraction 'b,
+          you have a borrow of type [&'a mut &'b mut], in the abstraction 'b,
           the outer loan is ignored, however you need to keep track of it so
           that when ending the borrow corresponding to 'a you can correctly
           project on the inner value).
        
           Example:
           ========
-          ```
-          fn f<'a,'b>(...) -> &'a mut &'b mut u32;
-          let x = f(...);
-          
-          > abs'a { a_mut_loan l0 (a_ignored_mut_loan l1 ⊥) }
-          > abs'b { a_ignored_mut_loan l0 (a_mut_loan l1 ⊥) }
-          > x -> mut_borrow l0 (mut_borrow l1 @s1)
-          ```
+          {[
+            fn f<'a,'b>(...) -> &'a mut &'b mut u32;
+            let x = f(...);
+
+            > abs'a { a_mut_loan l0 (a_ignored_mut_loan l1 ⊥) }
+            > abs'b { a_ignored_mut_loan l0 (a_mut_loan l1 ⊥) }
+            > x -> mut_borrow l0 (mut_borrow l1 @s1)
+          ]}
        *)
   | AEndedIgnoredMutLoan of {
       child : typed_avalue;
       given_back : typed_avalue;
       given_back_meta : mvalue;
     }
-      (** Similar to [AEndedMutLoan], for ignored loans.
+      (** Similar to {!AEndedMutLoan}, for ignored loans.
 
            Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
-           See the comment for [AEndedMutLoan].
+           See the comment for {!AEndedMutLoan}.
        *)
   | AIgnoredSharedLoan of typed_avalue
       (** An ignored shared loan.
             
           Example:
           ========
-          ```
-          fn f<'a,'b>(...) -> &'a &'b u32;
-          let x = f(...);
-          
-          > abs'a { a_shared_loan {l0} (shared_borrow l1) (a_ignored_shared_loan ⊥) }
-          > abs'b { a_ignored_shared_loan (a_shared_loan {l1} @s1 ⊥) }
-          > x -> shared_borrow l0
-          ```
+          {[
+            fn f<'a,'b>(...) -> &'a &'b u32;
+            let x = f(...);
+
+            > abs'a { a_shared_loan {l0} (shared_borrow l1) (a_ignored_shared_loan ⊥) }
+            > abs'b { a_ignored_shared_loan (a_shared_loan {l1} @s1 ⊥) }
+            > x -> shared_borrow l0
+          ]}
        *)
 
 (** Note that when a borrow content is ended, it is replaced by ⊥ (while
     we need to track ended loans more precisely, especially because of their
     children values).
 
-    Note that contrary to [aloan_content], here the children avalues are
+    Note that contrary to {!aloan_content}, here the children avalues are
     not independent of the parent avalues. For instance, a value
-    `AMutBorrow (_, AMutBorrow (_, ...)` (ignoring the types) really is
-    to be seen like a `mut_borrow ... (mut_borrow ...)`.
+    [AMutBorrow (_, AMutBorrow (_, ...)] (ignoring the types) really is
+    to be seen like a [mut_borrow ... (mut_borrow ...)].
     
     TODO: be more precise about the ignored borrows (keep track of the borrow
     ids)?
@@ -564,18 +566,18 @@ and aborrow_content =
 
           Example:
           ========
-          ```
-          fn f<'a>(px : &'a mut u32);
-          
-          > x -> mut_loan l0
-          > px -> mut_borrow l0 (U32 0)
-          
-          f(move px);
-          
-          > x -> mut_loan l0
-          > px -> ⊥
-          > abs0 { a_mut_borrow l0 (U32 0) }
-          ```
+          {[
+            fn f<'a>(px : &'a mut u32);
+
+            > x -> mut_loan l0
+            > px -> mut_borrow l0 (U32 0)
+
+            f(move px);
+
+            > x -> mut_loan l0
+            > px -> ⊥
+            > abs0 { a_mut_borrow l0 (U32 0) }
+          ]}
           
           The meta-value stores the initial value on which the projector was
           applied, which reduced to this mut borrow. This meta-information
@@ -587,18 +589,18 @@ and aborrow_content =
     
           Example:
           ========
-          ```
-          fn f<'a>(px : &'a u32);
-          
-          > x -> shared_loan {l0} (U32 0)
-          > px -> shared_borrow l0
-          
-          f(move px);
-          
-          > x -> shared_loan {l0} (U32 0)
-          > px -> ⊥
-          > abs0 { a_shared_borrow l0 }
-          ```
+          {[
+            fn f<'a>(px : &'a u32);
+
+            > x -> shared_loan {l0} (U32 0)
+            > px -> shared_borrow l0
+
+            f(move px);
+
+            > x -> shared_loan {l0} (U32 0)
+            > px -> ⊥
+            > abs0 { a_shared_borrow l0 }
+          ]}
      *)
   | AIgnoredMutBorrow of BorrowId.id option * typed_avalue
       (** An ignored mutable borrow.
@@ -614,42 +616,42 @@ and aborrow_content =
 
           Example:
           ========
-          ```
-          fn f<'a,'b>(ppx : &'a mut &'b mut u32);
-          
-          > x -> mut_loan l0
-          > px -> mut_loan l1
-          > ppx -> mut_borrow l1 (mut_borrow l0 (U32 0))
+          {[
+            fn f<'a,'b>(ppx : &'a mut &'b mut u32);
 
-          f(move ppx);
+            > x -> mut_loan l0
+            > px -> mut_loan l1
+            > ppx -> mut_borrow l1 (mut_borrow l0 (U32 0))
 
-          > x -> mut_loan l0
-          > px -> mut_loan l1
-          > ppx -> ⊥
-          > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication
-          > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) }
-          
-          ... // abs'a ends
-          
-          > x -> mut_loan l0
-          > px -> @s0
-          > ppx -> ⊥
-          > abs'b {
-          >   a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector
-          >                              (a_mut_borrow l0 (U32 0))
-          > }
-          
-          ... // `@s0` gets expanded to `&mut l2 @s1`
-
-          > x -> mut_loan l0
-          > px -> &mut l2 @s1
-          > ppx -> ⊥
-          > abs'b {
-          >   a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here
-          >                              (a_mut_borrow l0 (U32 0))
-          > }
-          
-          ```
+            f(move ppx);
+
+            > x -> mut_loan l0
+            > px -> mut_loan l1
+            > ppx -> ⊥
+            > abs'a { a_mut_borrow l1 (a_ignored_mut_borrow None (U32 0)) } // TODO: duplication
+            > abs'b {parents={abs'a}} { a_ignored_mut_borrow (Some l1) (a_mut_borrow l0 (U32 0)) }
+
+            ... // abs'a ends
+
+            > x -> mut_loan l0
+            > px -> @s0
+            > ppx -> ⊥
+            > abs'b {
+            >   a_ended_ignored_mut_borrow (a_proj_loans (@s0 <: &'b mut u32)) // <-- loan projector
+            >                              (a_mut_borrow l0 (U32 0))
+            > }
+
+            ... // [@s0] gets expanded to [&mut l2 @s1]
+
+            > x -> mut_loan l0
+            > px -> &mut l2 @s1
+            > ppx -> ⊥
+            > abs'b {
+            >   a_ended_ignored_mut_borrow (a_mut_loan l2) // <-- loan l2 is here
+            >                              (a_mut_borrow l0 (U32 0))
+            > }
+
+          ]}
 
           Note that we could use AIgnoredMutLoan in the case the borrow id is not
           None, which would allow us to simplify the rules (to not have rules
@@ -675,16 +677,16 @@ and aborrow_content =
             when generating the pure translation.
        *)
   | AEndedMutBorrow of msymbolic_value * typed_avalue
-      (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value
+      (** The sole purpose of {!AEndedMutBorrow} is to store the (symbolic) value
           that we gave back as a meta-value, to help with the synthesis.
 
-          We also remember the child [avalue] because this structural information
+          We also remember the child {!avalue} because this structural information
           is useful for the synthesis (but not for the symbolic execution):
           in practice the child value should only contain ended borrows, ignored
           values, bottom values, etc.
        *)
   | AEndedSharedBorrow
-      (** We don't really need [AEndedSharedBorrow]: we simply want to be
+      (** We don't really need {!AEndedSharedBorrow}: we simply want to be
           precise, and not insert ⊥ when ending borrows.
        *)
   | AEndedIgnoredMutBorrow of {
@@ -695,9 +697,9 @@ and aborrow_content =
               upon ending the borrow.
 
               Rk.: *DO NOT* use [visit_AEndedIgnoredMutLoan].
-              See the comment for [AEndedMutLoan].
+              See the comment for {!AEndedMutLoan}.
           *)
-    }  (** See the explanations for [AIgnoredMutBorrow] *)
+    }  (** See the explanations for {!AIgnoredMutBorrow} *)
   | AProjSharedBorrow of abstract_shared_borrows
       (** A projected shared borrow.
 
@@ -708,30 +710,30 @@ and aborrow_content =
 
           Example:
           ========
-          Below, when calling `f`, we need to introduce one shared borrow per
+          Below, when calling [f], we need to introduce one shared borrow per
           borrow in the argument.
-          ```
-          fn f<'a,'b>(pppx : &'a &'b &'c mut u32);
-
-          > x    -> mut_loan l0
-          > px   -> shared_loan {l1} (mut_borrow l0 (U32 0))
-          > ppx  -> shared_loan {l2} (shared_borrow l1)
-          > pppx -> shared_borrow l2
-
-          f(move pppx);
-
-          > x    -> mut_loan l0
-          > px   -> shared_loan {l1, l3, l4} (mut_borrow l0 (U32 0))
-          > ppx  -> shared_loan {l2} (shared_borrow l1)
-          > pppx -> ⊥
-          > abs'a { a_proj_shared_borrow {l2} }
-          > abs'b { a_proj_shared_borrow {l3} } // l3 reborrows l1
-          > abs'c { a_proj_shared_borrow {l4} } // l4 reborrows l0
-          ```
+          {[
+            fn f<'a,'b>(pppx : &'a &'b &'c mut u32);
+
+            > x    -> mut_loan l0
+            > px   -> shared_loan {l1} (mut_borrow l0 (U32 0))
+            > ppx  -> shared_loan {l2} (shared_borrow l1)
+            > pppx -> shared_borrow l2
+
+            f(move pppx);
+
+            > x    -> mut_loan l0
+            > px   -> shared_loan {l1, l3, l4} (mut_borrow l0 (U32 0))
+            > ppx  -> shared_loan {l2} (shared_borrow l1)
+            > pppx -> ⊥
+            > abs'a { a_proj_shared_borrow {l2} }
+            > abs'b { a_proj_shared_borrow {l3} } // l3 reborrows l1
+            > abs'c { a_proj_shared_borrow {l4} } // l4 reborrows l0
+          ]}
        *)
 
 (* TODO: the type of avalues doesn't make sense for loan avalues: they currently
-   are typed as `& (mut) T` instead of `T`...
+   are typed as [& (mut) T] instead of [T]...
 *)
 and typed_avalue = { value : avalue; ty : rty }
 [@@deriving
@@ -741,7 +743,7 @@ and typed_avalue = { value : avalue; ty : rty }
         name = "iter_typed_avalue";
         variety = "iter";
         ancestors = [ "iter_typed_avalue_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -749,7 +751,7 @@ and typed_avalue = { value : avalue; ty : rty }
         name = "map_typed_avalue";
         variety = "map";
         ancestors = [ "map_typed_avalue_base" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
 
@@ -764,6 +766,12 @@ type abs_kind =
           are currently synthesizing *)
 [@@deriving show]
 
+(** Abstractions model the parts in the borrow graph where the borrowing relations
+    have been abstracted because of a function call.
+    
+    In order to model the relations between the borrows, we use "abstraction values",
+    which are a special kind of value.
+*)
 type abs = {
   abs_id : (AbstractionId.id[@opaque]);
   call_id : (FunCallId.id[@opaque]);
@@ -789,7 +797,7 @@ type abs = {
           This allows to "pin" some regions, and is useful when generating
           backward functions.
           
-          For instance, if we have: `fn f<'a, 'b>(...) -> (&'a mut T, &'b mut T)`,
+          For instance, if we have: [fn f<'a, 'b>(...) -> (&'a mut T, &'b mut T)],
           when generating the backward function for 'a, we have to make sure we
           don't need to end the return region for 'b (if it is the case, it means
           the function doesn't borrow check).
@@ -810,7 +818,7 @@ type abs = {
         name = "iter_abs";
         variety = "iter";
         ancestors = [ "iter_typed_avalue" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       },
     visitors
@@ -818,15 +826,9 @@ type abs = {
         name = "map_abs";
         variety = "map";
         ancestors = [ "map_typed_avalue" ];
-        nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+        nude = true (* Don't inherit {!VisitorsRuntime.iter} *);
         concrete = true;
       }]
-(** Abstractions model the parts in the borrow graph where the borrowing relations
-    have been abstracted because of a function call.
-    
-    In order to model the relations between the borrows, we use "abstraction values",
-    which are a special kind of value.
-*)
 
 (** A symbolic expansion
     
diff --git a/src/ValuesUtils.ml b/src/ValuesUtils.ml
index bc205622..72d7abe0 100644
--- a/src/ValuesUtils.ml
+++ b/src/ValuesUtils.ml
@@ -4,8 +4,8 @@ open Types
 open Values
 module TA = TypesAnalysis
 
-exception FoundSymbolicValue of symbolic_value
 (** Utility exception *)
+exception FoundSymbolicValue of symbolic_value
 
 let mk_unit_value : typed_value =
   { value = Adt { variant_id = None; field_values = [] }; ty = mk_unit_ty }
@@ -112,8 +112,8 @@ let find_first_primitively_copyable_sv_with_borrows (type_infos : TA.type_infos)
 
 (** Strip the outer shared loans in a value.
     Ex.:
-    `shared_loan {l0, l1} (3 : u32, shared_loan {l2} (4 : u32))` ~~>
-    `(3 : u32, shared_loan {l2} (4 : u32))`
+    [shared_loan {l0, l1} (3 : u32, shared_loan {l2} (4 : u32))] ~~>
+    [(3 : u32, shared_loan {l2} (4 : u32))]
  *)
 let rec value_strip_shared_loans (v : typed_value) : typed_value =
   match v.value with