6 files changed, 19 insertions, 17 deletions
diff --git a/compiler/ExtractToFStar.ml b/compiler/ExtractToFStar.ml
index a77e3df3..b44b8f25 100644
--- a/compiler/ExtractToFStar.ml
+++ b/compiler/ExtractToFStar.ml
@@ -857,7 +857,7 @@ let extract_global (ctx : extraction_ctx) (fmt : F.formatter)
     (id : A.GlobalDeclId.id) : unit =
   F.pp_print_string fmt (ctx_get_global id ctx)
 
-(** [inside]: see [extract_ty].
+(** [inside]: see {!extract_ty}.
 
     As a pattern can introduce new variables, we return an extraction context
     updated with new bindings.
diff --git a/compiler/InterpreterBorrows.ml b/compiler/InterpreterBorrows.ml
index 30c3b221..16f68d9e 100644
--- a/compiler/InterpreterBorrows.ml
+++ b/compiler/InterpreterBorrows.ml
@@ -224,7 +224,7 @@ let end_borrow_get_borrow (allowed_abs : V.AbstractionId.id option)
     Ok (ctx, !replaced_bc)
   with FoundPriority outers -> Error outers
 
-(** Auxiliary function to end borrows. See [give_back].
+(** Auxiliary function to end borrows. See {!give_back}.
     
     When we end a mutable borrow, we need to "give back" the value it contained
     to its original owner by reinserting it at the proper position.
@@ -475,7 +475,7 @@ let give_back_symbolic_value (_config : C.config)
   in
   update_intersecting_aproj_loans proj_regions proj_ty sv subst ctx
 
-(** Auxiliary function to end borrows. See [give_back].
+(** Auxiliary function to end borrows. See {!give_back}.
 
     This function is similar to {!give_back_value} but gives back an {!V.avalue}
     (coming from an abstraction).
@@ -577,7 +577,7 @@ let give_back_avalue_to_same_abstraction (_config : C.config)
   (* Return *)
   ctx
 
-(** Auxiliary function to end borrows. See [give_back].
+(** Auxiliary function to end borrows. See  {!give_back}.
     
     When we end a shared borrow, we need to remove the borrow id from the list
     of borrows to the shared value.
@@ -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] *)
+(** 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 *)
@@ -1430,7 +1430,7 @@ let end_outer_borrow config : V.BorrowId.id -> cm_fun =
 let end_outer_borrows config : V.BorrowId.Set.t -> cm_fun =
   end_borrows config [] None
 
-(** Helper function: see [activate_inactivated_mut_borrow].
+(** Helper function: see {!activate_inactivated_mut_borrow}.
 
     This function updates the shared loan to a mutable loan (we then update
     the borrow with another helper). Of course, the shared loan must contain
diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index 8caa828e..9a944428 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -431,7 +431,7 @@ let expand_symbolic_value_borrow (config : C.config)
 
     Apply a branching symbolic expansion to a context and execute all the
     branches. Note that the expansion is optional for every branch (this is
-    used for integer expansion: see [expand_symbolic_int]).
+    used for integer expansion: see {!expand_symbolic_int}).
     
     [see_cf_l]: list of pairs (optional symbolic expansion, continuation)
 *)
diff --git a/compiler/InterpreterPaths.ml b/compiler/InterpreterPaths.ml
index 28e81dc6..1cd27b31 100644
--- a/compiler/InterpreterPaths.ml
+++ b/compiler/InterpreterPaths.ml
@@ -620,9 +620,11 @@ 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])
-    - if false: only end the outer loans. This is used by [assign_to_place]
+      ones. This is used when evaluating the {!LlbcAst.Drop} statement (see {!InterpreterStatements.drop_value})
+    - if false: only end the outer loans. This is used by {!InterpreterStatements.assign_to_place}
       or to drop the loans in the local variables when popping a frame.
+    TODO: remove this option, it is actually not used anymore (should always be
+    false).
 
     Note that we don't do what is defined in the formalization: we move the
     value to a temporary dummy value, then explore this value and end the
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 45d2aab2..f935734e 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -413,13 +413,13 @@ let pop_frame_assign (config : C.config) (dest : E.place) : cm_fun =
   in
   comp cf_pop cf_assign
 
-(** Auxiliary function - see [eval_non_local_function_call] *)
+(** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_replace_concrete (_config : C.config)
     (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun
     =
  fun _cf _ctx -> raise Unimplemented
 
-(** Auxiliary function - see [eval_non_local_function_call] *)
+(** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_new_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
  fun cf ctx ->
@@ -459,7 +459,7 @@ let eval_box_new_concrete (config : C.config)
   | _ -> 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] *)
+    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 =
@@ -504,19 +504,19 @@ let eval_box_deref_mut_or_shared_concrete (config : C.config)
       comp cf_borrow cf_move cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function - see [eval_non_local_function_call] *)
+(** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_deref_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
   let is_mut = false in
   eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut
 
-(** Auxiliary function - see [eval_non_local_function_call] *)
+(** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_box_deref_mut_concrete (config : C.config)
     (region_params : T.erased_region list) (type_params : T.ety list) : cm_fun =
   let is_mut = true in
   eval_box_deref_mut_or_shared_concrete config region_params type_params is_mut
 
-(** Auxiliary function - see [eval_non_local_function_call].
+(** Auxiliary function - see {!eval_non_local_function_call}.
 
     [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,
@@ -556,7 +556,7 @@ let eval_box_free (config : C.config) (region_params : T.erased_region list)
       cc cf ctx
   | _ -> raise (Failure "Inconsistent state")
 
-(** Auxiliary function - see [eval_non_local_function_call] *)
+(** Auxiliary function - see {!eval_non_local_function_call} *)
 let eval_vec_function_concrete (_config : C.config) (_fid : A.assumed_fun_id)
     (_region_params : T.erased_region list) (_type_params : T.ety list) : cm_fun
     =
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 3edae38a..5da07e55 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -100,7 +100,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator =
   let id = obj#visit_expression () body.body.e () in
   VarId.generator_from_incr_id id
 
-(** "pretty-name context": see [compute_pretty_names] *)
+(** "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 *)